:: LATTICE2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem :: LATTICE2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th2: :: LATTICE2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set
for C being non empty set
for B being Subset of A
for g being Function of A,C holds dom (g | B) = B
proof end;

theorem :: LATTICE2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: LATTICE2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th5: :: LATTICE2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set
for C being non empty set
for B being Subset of A
for f, g being Function of A,C holds
( f | B = g | B iff for x being Element of A st x in B holds
g . x = f . x )
proof end;

theorem Th6: :: LATTICE2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set
for C being non empty set
for f, g being Function of A,C
for B being set holds f +* (g | B) is Function of A,C
proof end;

theorem Th7: :: LATTICE2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set
for C being non empty set
for B being Subset of A
for g, f being Function of A,C holds (g | B) +* f = f
proof end;

theorem Th8: :: LATTICE2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being Function st g <= f holds
f +* g = f
proof end;

theorem Th9: :: LATTICE2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set
for C being non empty set
for B being Subset of A
for f being Function of A,C holds f +* (f | B) = f
proof end;

theorem Th10: :: LATTICE2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set
for C being non empty set
for B being Subset of A
for g, f being Function of A,C st ( for x being Element of A st x in B holds
g . x = f . x ) holds
f +* (g | B) = f
proof end;

theorem :: LATTICE2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: LATTICE2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set
for C being non empty set
for g, f being Function of A,C
for B being Finite_Subset of A holds (g | B) +* f = f
proof end;

theorem Th13: :: LATTICE2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set
for C being non empty set
for g being Function of A,C
for B being Finite_Subset of A holds dom (g | B) = B
proof end;

theorem Th14: :: LATTICE2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set
for C being non empty set
for g, f being Function of A,C
for B being Finite_Subset of A st ( for x being Element of A st x in B holds
g . x = f . x ) holds
f +* (g | B) = f
proof end;

theorem :: LATTICE2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th16: :: LATTICE2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set
for C being non empty set
for f, g being Function of A,C
for B being Finite_Subset of A st f | B = g | B holds
f .: B = g .: B
proof end;

definition
let D be non empty set ;
let o, o' be BinOp of D;
pred o absorbs o' means :Def1: :: LATTICE2:def 1
for x, y being Element of D holds o . x,(o' . x,y) = x;
end;

:: deftheorem Def1 defines absorbs LATTICE2:def 1 :
for D being non empty set
for o, o' being BinOp of D holds
( o absorbs o' iff for x, y being Element of D holds o . x,(o' . x,y) = x );

notation
let D be non empty set ;
let o, o' be BinOp of D;
antonym o doesn't_absorb o' for o absorbs o';
end;

theorem Th17: :: LATTICE2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty LattStr st the L_join of L is commutative & the L_join of L is associative & the L_meet of L is commutative & the L_meet of L is associative & the L_join of L absorbs the L_meet of L & the L_meet of L absorbs the L_join of L holds
L is Lattice-like
proof end;

definition
let L be LattStr ;
func L .: -> strict LattStr equals :: LATTICE2:def 2
LattStr(# the carrier of L,the L_meet of L,the L_join of L #);
correctness
coherence
LattStr(# the carrier of L,the L_meet of L,the L_join of L #) is strict LattStr
;
;
end;

:: deftheorem defines .: LATTICE2:def 2 :
for L being LattStr holds L .: = LattStr(# the carrier of L,the L_meet of L,the L_join of L #);

registration
let L be non empty LattStr ;
cluster L .: -> non empty strict ;
coherence
not L .: is empty
;
end;

theorem :: LATTICE2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty LattStr holds
( the carrier of L = the carrier of (L .: ) & the L_join of L = the L_meet of (L .: ) & the L_meet of L = the L_join of (L .: ) ) ;

theorem :: LATTICE2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty strict LattStr holds (L .: ) .: = L ;

theorem :: LATTICE2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th21: :: LATTICE2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for u being Element of L st ( for v being Element of L holds u "\/" v = v ) holds
u = Bottom L
proof end;

theorem Th22: :: LATTICE2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for u being Element of L st ( for v being Element of L holds the L_join of L . u,v = v ) holds
u = Bottom L
proof end;

theorem :: LATTICE2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th24: :: LATTICE2:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for u being Element of L st ( for v being Element of L holds u "/\" v = v ) holds
u = Top L
proof end;

theorem Th25: :: LATTICE2:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for u being Element of L st ( for v being Element of L holds the L_meet of L . u,v = v ) holds
u = Top L
proof end;

theorem Th26: :: LATTICE2:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice holds the L_join of L is idempotent
proof end;

theorem Th27: :: LATTICE2:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty join-commutative \/-SemiLattStr holds the L_join of L is commutative
proof end;

theorem Th28: :: LATTICE2:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice st the L_join of L has_a_unity holds
Bottom L = the_unity_wrt the L_join of L
proof end;

theorem Th29: :: LATTICE2:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty join-associative \/-SemiLattStr holds the L_join of L is associative
proof end;

theorem Th30: :: LATTICE2:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice holds the L_meet of L is idempotent
proof end;

theorem Th31: :: LATTICE2:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty meet-commutative /\-SemiLattStr holds the L_meet of L is commutative
proof end;

theorem Th32: :: LATTICE2:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty meet-associative /\-SemiLattStr holds the L_meet of L is associative
proof end;

registration
let L be non empty join-commutative \/-SemiLattStr ;
cluster the L_join of L -> commutative ;
coherence
the L_join of L is commutative
by Th27;
end;

registration
let L be non empty join-associative \/-SemiLattStr ;
cluster the L_join of L -> associative ;
coherence
the L_join of L is associative
by Th29;
end;

registration
let L be non empty meet-commutative /\-SemiLattStr ;
cluster the L_meet of L -> commutative ;
coherence
the L_meet of L is commutative
by Th31;
end;

registration
let L be non empty meet-associative /\-SemiLattStr ;
cluster the L_meet of L -> associative ;
coherence
the L_meet of L is associative
by Th32;
end;

theorem Th33: :: LATTICE2:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice st the L_meet of L has_a_unity holds
Top L = the_unity_wrt the L_meet of L
proof end;

theorem Th34: :: LATTICE2:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice holds the L_join of L is_distributive_wrt the L_join of L
proof end;

theorem :: LATTICE2:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice st L is D_Lattice holds
the L_join of L is_distributive_wrt the L_meet of L
proof end;

theorem Th36: :: LATTICE2:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice st the L_join of L is_distributive_wrt the L_meet of L holds
L is distributive
proof end;

theorem Th37: :: LATTICE2:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice st L is D_Lattice holds
the L_meet of L is_distributive_wrt the L_join of L
proof end;

theorem :: LATTICE2:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice st the L_meet of L is_distributive_wrt the L_join of L holds
L is distributive
proof end;

theorem Th39: :: LATTICE2:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice holds the L_meet of L is_distributive_wrt the L_meet of L
proof end;

theorem Th40: :: LATTICE2:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice holds the L_join of L absorbs the L_meet of L
proof end;

theorem Th41: :: LATTICE2:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice holds the L_meet of L absorbs the L_join of L
proof end;

definition
let A be non empty set ;
let L be Lattice;
let B be Finite_Subset of A;
let f be Function of A,the carrier of L;
func FinJoin B,f -> Element of L equals :: LATTICE2:def 3
the L_join of L $$ B,f;
correctness
coherence
the L_join of L $$ B,f is Element of L
;
;
func FinMeet B,f -> Element of L equals :: LATTICE2:def 4
the L_meet of L $$ B,f;
correctness
coherence
the L_meet of L $$ B,f is Element of L
;
;
end;

:: deftheorem defines FinJoin LATTICE2:def 3 :
for A being non empty set
for L being Lattice
for B being Finite_Subset of A
for f being Function of A,the carrier of L holds FinJoin B,f = the L_join of L $$ B,f;

:: deftheorem defines FinMeet LATTICE2:def 4 :
for A being non empty set
for L being Lattice
for B being Finite_Subset of A
for f being Function of A,the carrier of L holds FinMeet B,f = the L_meet of L $$ B,f;

theorem :: LATTICE2:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th43: :: LATTICE2:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for A being non empty set
for x being Element of A
for B being Finite_Subset of A
for f being Function of A,the carrier of L st x in B holds
f . x [= FinJoin B,f
proof end;

theorem Th44: :: LATTICE2:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for u being Element of L
for A being non empty set
for B being Finite_Subset of A
for f being Function of A,the carrier of L st ex x being Element of A st
( x in B & u [= f . x ) holds
u [= FinJoin B,f
proof end;

theorem Th45: :: LATTICE2:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for u being Element of L
for A being non empty set
for B being Finite_Subset of A
for f being Function of A,the carrier of L st ( for x being Element of A st x in B holds
f . x = u ) & B <> {} holds
FinJoin B,f = u
proof end;

theorem :: LATTICE2:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for u being Element of L
for A being non empty set
for B being Finite_Subset of A
for f being Function of A,the carrier of L st FinJoin B,f [= u holds
for x being Element of A st x in B holds
f . x [= u
proof end;

theorem Th47: :: LATTICE2:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for u being Element of L
for A being non empty set
for B being Finite_Subset of A
for f being Function of A,the carrier of L st B <> {} & ( for x being Element of A st x in B holds
f . x [= u ) holds
FinJoin B,f [= u
proof end;

theorem :: LATTICE2:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for A being non empty set
for B being Finite_Subset of A
for f, g being Function of A,the carrier of L st B <> {} & ( for x being Element of A st x in B holds
f . x [= g . x ) holds
FinJoin B,f [= FinJoin B,g
proof end;

theorem Th49: :: LATTICE2:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for A being non empty set
for B being Finite_Subset of A
for f, g being Function of A,the carrier of L st B <> {} & f | B = g | B holds
FinJoin B,f = FinJoin B,g
proof end;

theorem :: LATTICE2:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for v being Element of L
for A being non empty set
for B being Finite_Subset of A
for f being Function of A,the carrier of L st B <> {} holds
v "\/" (FinJoin B,f) = FinJoin B,(the L_join of L [;] v,f)
proof end;

registration
let L be Lattice;
cluster L .: -> non empty strict Lattice-like ;
coherence
L .: is Lattice-like
proof end;
end;

theorem :: LATTICE2:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for L being Lattice
for B being Finite_Subset of A
for f being Function of A,the carrier of L
for f' being Function of A,the carrier of (L .: ) st f = f' holds
( FinJoin B,f = FinMeet B,f' & FinMeet B,f = FinJoin B,f' ) ;

theorem Th52: :: LATTICE2:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for a, b being Element of L
for a', b' being Element of (L .: ) st a = a' & b = b' holds
( a "/\" b = a' "\/" b' & a "\/" b = a' "/\" b' ) ;

theorem Th53: :: LATTICE2:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for a, b being Element of L st a [= b holds
for a', b' being Element of (L .: ) st a = a' & b = b' holds
b' [= a'
proof end;

theorem Th54: :: LATTICE2:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for a, b being Element of L
for a', b' being Element of (L .: ) st a' [= b' & a = a' & b = b' holds
b [= a
proof end;

theorem Th55: :: LATTICE2:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for A being non empty set
for x being Element of A
for B being Finite_Subset of A
for f being Function of A,the carrier of L st x in B holds
FinMeet B,f [= f . x
proof end;

theorem Th56: :: LATTICE2:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for u being Element of L
for A being non empty set
for B being Finite_Subset of A
for f being Function of A,the carrier of L st ex x being Element of A st
( x in B & f . x [= u ) holds
FinMeet B,f [= u
proof end;

theorem :: LATTICE2:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for u being Element of L
for A being non empty set
for B being Finite_Subset of A
for f being Function of A,the carrier of L st ( for x being Element of A st x in B holds
f . x = u ) & B <> {} holds
FinMeet B,f = u
proof end;

theorem :: LATTICE2:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for v being Element of L
for A being non empty set
for B being Finite_Subset of A
for f being Function of A,the carrier of L st B <> {} holds
v "/\" (FinMeet B,f) = FinMeet B,(the L_meet of L [;] v,f)
proof end;

theorem :: LATTICE2:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for u being Element of L
for A being non empty set
for B being Finite_Subset of A
for f being Function of A,the carrier of L st u [= FinMeet B,f holds
for x being Element of A st x in B holds
u [= f . x
proof end;

theorem :: LATTICE2:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for A being non empty set
for B being Finite_Subset of A
for f, g being Function of A,the carrier of L st B <> {} & f | B = g | B holds
FinMeet B,f = FinMeet B,g
proof end;

theorem Th61: :: LATTICE2:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for u being Element of L
for A being non empty set
for B being Finite_Subset of A
for f being Function of A,the carrier of L st B <> {} & ( for x being Element of A st x in B holds
u [= f . x ) holds
u [= FinMeet B,f
proof end;

theorem :: LATTICE2:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice
for A being non empty set
for B being Finite_Subset of A
for f, g being Function of A,the carrier of L st B <> {} & ( for x being Element of A st x in B holds
f . x [= g . x ) holds
FinMeet B,f [= FinMeet B,g
proof end;

theorem :: LATTICE2:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice holds
( L is lower-bounded iff L .: is upper-bounded )
proof end;

theorem Th64: :: LATTICE2:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice holds
( L is upper-bounded iff L .: is lower-bounded )
proof end;

theorem :: LATTICE2:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice holds
( L is D_Lattice iff L .: is D_Lattice )
proof end;

theorem Th66: :: LATTICE2:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being 0_Lattice holds Bottom L is_a_unity_wrt the L_join of L
proof end;

theorem Th67: :: LATTICE2:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being 0_Lattice holds the L_join of L has_a_unity
proof end;

theorem Th68: :: LATTICE2:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being 0_Lattice holds Bottom L = the_unity_wrt the L_join of L
proof end;

theorem Th69: :: LATTICE2:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for B being Finite_Subset of A
for L being 0_Lattice
for f, g being Function of A,the carrier of L st f | B = g | B holds
FinJoin B,f = FinJoin B,g
proof end;

theorem Th70: :: LATTICE2:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for B being Finite_Subset of A
for L being 0_Lattice
for f being Function of A,the carrier of L
for u being Element of L st ( for x being Element of A st x in B holds
f . x [= u ) holds
FinJoin B,f [= u
proof end;

theorem :: LATTICE2:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for B being Finite_Subset of A
for L being 0_Lattice
for f, g being Function of A,the carrier of L st ( for x being Element of A st x in B holds
f . x [= g . x ) holds
FinJoin B,f [= FinJoin B,g
proof end;

theorem Th72: :: LATTICE2:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being 1_Lattice holds Top L is_a_unity_wrt the L_meet of L
proof end;

theorem Th73: :: LATTICE2:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being 1_Lattice holds the L_meet of L has_a_unity
proof end;

theorem :: LATTICE2:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being 1_Lattice holds Top L = the_unity_wrt the L_meet of L
proof end;

theorem :: LATTICE2:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for B being Finite_Subset of A
for L being 1_Lattice
for f, g being Function of A,the carrier of L st f | B = g | B holds
FinMeet B,f = FinMeet B,g
proof end;

theorem Th76: :: LATTICE2:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for B being Finite_Subset of A
for L being 1_Lattice
for f being Function of A,the carrier of L
for u being Element of L st ( for x being Element of A st x in B holds
u [= f . x ) holds
u [= FinMeet B,f
proof end;

theorem :: LATTICE2:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for B being Finite_Subset of A
for L being 1_Lattice
for f, g being Function of A,the carrier of L st ( for x being Element of A st x in B holds
f . x [= g . x ) holds
FinMeet B,f [= FinMeet B,g
proof end;

theorem :: LATTICE2:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being 0_Lattice holds Bottom L = Top (L .: )
proof end;

theorem :: LATTICE2:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being 1_Lattice holds Top L = Bottom (L .: )
proof end;

definition
mode D0_Lattice is distributive lower-bounded Lattice;
end;

theorem :: LATTICE2:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being D0_Lattice holds the L_meet of L is_distributive_wrt the L_join of L by Th37;

theorem Th81: :: LATTICE2:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for B being Finite_Subset of A
for L being D0_Lattice
for f being Function of A,the carrier of L
for u being Element of L holds the L_meet of L . u,(FinJoin B,f) = FinJoin B,(the L_meet of L [;] u,f)
proof end;

theorem :: LATTICE2:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for B being Finite_Subset of A
for L being D0_Lattice
for g, f being Function of A,the carrier of L
for u being Element of L st ( for x being Element of A st x in B holds
g . x = u "/\" (f . x) ) holds
u "/\" (FinJoin B,f) = FinJoin B,g
proof end;

theorem Th83: :: LATTICE2:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for B being Finite_Subset of A
for L being D0_Lattice
for f being Function of A,the carrier of L
for u being Element of L holds u "/\" (FinJoin B,f) = FinJoin B,(the L_meet of L [;] u,f) by Th81;

definition
let IT be Lattice;
canceled;
attr IT is Heyting means :Def6: :: LATTICE2:def 6
( IT is implicative & IT is lower-bounded );
end;

:: deftheorem LATTICE2:def 5 :
canceled;

:: deftheorem Def6 defines Heyting LATTICE2:def 6 :
for IT being Lattice holds
( IT is Heyting iff ( IT is implicative & IT is lower-bounded ) );

registration
cluster Heyting LattStr ;
existence
ex b1 being Lattice st b1 is Heyting
proof end;
end;

registration
cluster Heyting -> lower-bounded implicative LattStr ;
coherence
for b1 being Lattice st b1 is Heyting holds
( b1 is implicative & b1 is lower-bounded )
by Def6;
cluster lower-bounded implicative -> Heyting LattStr ;
coherence
for b1 being Lattice st b1 is implicative & b1 is lower-bounded holds
b1 is Heyting
by Def6;
end;

definition
mode H_Lattice is Heyting Lattice;
end;

registration
cluster strict lower-bounded implicative Heyting LattStr ;
existence
ex b1 being Lattice st
( b1 is Heyting & b1 is strict )
proof end;
end;

theorem :: LATTICE2:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being 0_Lattice holds
( L is H_Lattice iff for x, z being Element of L ex y being Element of L st
( x "/\" y [= z & ( for v being Element of L st x "/\" v [= z holds
v [= y ) ) )
proof end;

theorem :: LATTICE2:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Lattice holds
( L is finite iff L .: is finite )
proof end;

Lm1: for L being Lattice st L is finite holds
L is lower-bounded
proof end;

Lm2: for L being Lattice st L is finite holds
L is upper-bounded
proof end;

registration
cluster finite -> lower-bounded LattStr ;
coherence
for b1 being Lattice st b1 is finite holds
b1 is lower-bounded
by Lm1;
cluster finite -> upper-bounded LattStr ;
coherence
for b1 being Lattice st b1 is finite holds
b1 is upper-bounded
by Lm2;
end;

registration
cluster finite -> bounded LattStr ;
coherence
for b1 being Lattice st b1 is finite holds
b1 is bounded
proof end;
end;

registration
cluster finite distributive -> lower-bounded implicative Heyting LattStr ;
coherence
for b1 being Lattice st b1 is distributive & b1 is finite holds
b1 is Heyting
proof end;
end;