begin
theorem
canceled;
theorem
canceled;
theorem
for
X being
set st
X <> {} & ( for
Z being
set st
Z <> {} &
Z c= X &
Z is
c=-linear holds
ex
Y being
set st
(
Y in X & ( for
X1 being
set st
X1 in Z holds
X1 c= Y ) ) ) holds
ex
Y being
set st
(
Y in X & ( for
Z being
set st
Z in X &
Z <> Y holds
not
Y c= Z ) )
begin
theorem
canceled;
theorem
theorem
:: deftheorem Def1 defines Homomorphism LATTICE4:def 1 :
for L1, L2 being Lattice
for b3 being Function of the carrier of L1,the carrier of L2 holds
( b3 is Homomorphism of L1,L2 iff for a1, b1 being Element of L1 holds
( b3 . (a1 "\/" b1) = (b3 . a1) "\/" (b3 . b1) & b3 . (a1 "/\" b1) = (b3 . a1) "/\" (b3 . b1) ) );
theorem Th7:
theorem Th8:
theorem Th9:
:: deftheorem LATTICE4:def 2 :
canceled;
:: deftheorem LATTICE4:def 3 :
canceled;
:: deftheorem LATTICE4:def 4 :
canceled;
:: deftheorem defines are_isomorphic LATTICE4:def 5 :
for L1, L2 being Lattice holds
( L1,L2 are_isomorphic iff ex f being Homomorphism of L1,L2 st f is bijective );
:: deftheorem Def6 defines preserves_implication LATTICE4:def 6 :
for L1, L2 being Lattice
for f being Homomorphism of L1,L2 holds
( f preserves_implication iff for a1, b1 being Element of L1 holds f . (a1 => b1) = (f . a1) => (f . b1) );
:: deftheorem Def7 defines preserves_top LATTICE4:def 7 :
for L1, L2 being Lattice
for f being Homomorphism of L1,L2 holds
( f preserves_top iff f . (Top L1) = Top L2 );
:: deftheorem Def8 defines preserves_bottom LATTICE4:def 8 :
for L1, L2 being Lattice
for f being Homomorphism of L1,L2 holds
( f preserves_bottom iff f . (Bottom L1) = Bottom L2 );
:: deftheorem Def9 defines preserves_complement LATTICE4:def 9 :
for L1, L2 being Lattice
for f being Homomorphism of L1,L2 holds
( f preserves_complement iff for a1 being Element of L1 holds f . (a1 ` ) = (f . a1) ` );
:: deftheorem LATTICE4:def 10 :
canceled;
theorem Th10:
theorem
:: deftheorem LATTICE4:def 11 :
canceled;
:: deftheorem defines FinJoin LATTICE4:def 12 :
for L being Lattice
for B being Finite_Subset of the carrier of L holds FinJoin B = FinJoin B,(id L);
:: deftheorem defines FinMeet LATTICE4:def 13 :
for L being Lattice
for B being Finite_Subset of the carrier of L holds FinMeet B = FinMeet B,(id L);
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th16:
theorem Th17:
begin
theorem Th18:
begin
theorem Th19:
theorem Th20:
theorem Th21:
theorem
Lm1:
for 0L being lower-bounded Lattice
for f being Function of the carrier of 0L,the carrier of 0L holds FinJoin ({}. the carrier of 0L),f = Bottom 0L
theorem
theorem Th24:
begin
theorem Th25:
Lm2:
for 1L being upper-bounded Lattice
for f being Function of the carrier of 1L,the carrier of 1L holds FinMeet ({}. the carrier of 1L),f = Top 1L
theorem
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
begin
Lm3:
for DL being distributive upper-bounded Lattice
for B being Finite_Subset of the carrier of DL
for p being Element of DL
for f being UnOp of the carrier of DL holds the L_join of DL . (the L_meet of DL $$ B,f),p = the L_meet of DL $$ B,(the L_join of DL [:] f,p)
theorem Th32:
begin
theorem Th33:
theorem Th34:
theorem
begin
theorem Th36:
theorem Th37:
theorem
:: deftheorem Def14 defines Field LATTICE4:def 14 :
for BL being Boolean Lattice
for b2 being non empty Subset of BL holds
( b2 is Field of BL iff for a, b being Element of BL st a in b2 & b in b2 holds
( a "/\" b in b2 & a ` in b2 ) );
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
:: deftheorem Def15 defines field_by LATTICE4:def 15 :
for BL being Boolean Lattice
for A being non empty Subset of BL
for b3 being Field of BL holds
( b3 = field_by A iff ( A c= b3 & ( for F being Field of BL st A c= F holds
b3 c= F ) ) );
:: deftheorem defines SetImp LATTICE4:def 16 :
for BL being Boolean Lattice
for A being non empty Subset of BL holds SetImp A = { (a => b) where a, b is Element of BL : ( a in A & b in A ) } ;
theorem
theorem Th44:
:: deftheorem Def17 defines comp LATTICE4:def 17 :
for BL being Boolean Lattice
for b2 being Function of the carrier of BL,the carrier of BL holds
( b2 = comp BL iff for a being Element of BL holds b2 . a = a ` );
theorem Th45:
theorem
theorem
theorem Th48:
theorem Th49:
theorem