:: LATTICE4 semantic presentation
begin
theorem :: LATTICE4:1
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 ) )
proof
let X be set ; ::_thesis: ( 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 ) ) ) implies ex Y being set st
( Y in X & ( for Z being set st Z in X & Z <> Y holds
not Y c= Z ) ) )
assume that
A1: X <> {} and
A2: 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 ) ) ; ::_thesis: ex Y being set st
( Y in X & ( for Z being set st Z in X & Z <> Y holds
not Y c= Z ) )
for Z being set st 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 ) )
proof
let Z be set ; ::_thesis: ( Z c= X & Z is c=-linear implies ex Y being set st
( Y in X & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) )
assume A3: ( Z c= X & Z is c=-linear ) ; ::_thesis: ex Y being set st
( Y in X & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
percases ( Z = {} or Z <> {} ) ;
supposeA4: Z = {} ; ::_thesis: ex Y being set st
( Y in X & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
set Y = the Element of X;
for X1 being set st X1 in Z holds
X1 c= the Element of X by A4;
hence ex Y being set st
( Y in X & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) by A1; ::_thesis: verum
end;
suppose Z <> {} ; ::_thesis: ex Y being set st
( Y in X & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
hence ex Y being set st
( Y in X & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) by A2, A3; ::_thesis: verum
end;
end;
end;
hence ex Y being set st
( Y in X & ( for Z being set st Z in X & Z <> Y holds
not Y c= Z ) ) by A1, ORDERS_1:65; ::_thesis: verum
end;
begin
registration
let L be Lattice;
cluster<.L.) -> prime ;
coherence
<.L.) is prime
proof
let p be Element of L; :: according to FILTER_0:def_5 ::_thesis: for b1 being Element of the carrier of L holds
( ( not p "\/" b1 in <.L.) or p in <.L.) or b1 in <.L.) ) & ( ( not p in <.L.) & not b1 in <.L.) ) or p "\/" b1 in <.L.) ) )
thus for b1 being Element of the carrier of L holds
( ( not p "\/" b1 in <.L.) or p in <.L.) or b1 in <.L.) ) & ( ( not p in <.L.) & not b1 in <.L.) ) or p "\/" b1 in <.L.) ) ) ; ::_thesis: verum
end;
end;
theorem :: LATTICE4:2
for L being Lattice
for F, H being Filter of L holds
( F c= <.(F \/ H).) & H c= <.(F \/ H).) )
proof
let L be Lattice; ::_thesis: for F, H being Filter of L holds
( F c= <.(F \/ H).) & H c= <.(F \/ H).) )
let F, H be Filter of L; ::_thesis: ( F c= <.(F \/ H).) & H c= <.(F \/ H).) )
A1: F \/ H c= <.(F \/ H).) by FILTER_0:def_4;
( F c= F \/ H & H c= F \/ H ) by XBOOLE_1:7;
hence ( F c= <.(F \/ H).) & H c= <.(F \/ H).) ) by A1, XBOOLE_1:1; ::_thesis: verum
end;
theorem :: LATTICE4:3
for L being Lattice
for F being Filter of L
for p, q being Element of L st p in <.(<.q.) \/ F).) holds
ex r being Element of L st
( r in F & q "/\" r [= p )
proof
let L be Lattice; ::_thesis: for F being Filter of L
for p, q being Element of L st p in <.(<.q.) \/ F).) holds
ex r being Element of L st
( r in F & q "/\" r [= p )
let F be Filter of L; ::_thesis: for p, q being Element of L st p in <.(<.q.) \/ F).) holds
ex r being Element of L st
( r in F & q "/\" r [= p )
let p, q be Element of L; ::_thesis: ( p in <.(<.q.) \/ F).) implies ex r being Element of L st
( r in F & q "/\" r [= p ) )
A1: <.(<.q.) \/ F).) = { r where r is Element of L : ex p9, q9 being Element of L st
( p9 "/\" q9 [= r & p9 in <.q.) & q9 in F ) } by FILTER_0:35;
assume p in <.(<.q.) \/ F).) ; ::_thesis: ex r being Element of L st
( r in F & q "/\" r [= p )
then ex r being Element of L st
( r = p & ex p9, q9 being Element of L st
( p9 "/\" q9 [= r & p9 in <.q.) & q9 in F ) ) by A1;
then consider p9, q9 being Element of L such that
A2: p9 "/\" q9 [= p and
A3: p9 in <.q.) and
A4: q9 in F ;
q [= p9 by A3, FILTER_0:15;
then q "/\" q9 [= p9 "/\" q9 by LATTICES:9;
hence ex r being Element of L st
( r in F & q "/\" r [= p ) by A2, A4, LATTICES:7; ::_thesis: verum
end;
definition
let L1, L2 be Lattice;
mode Homomorphism of L1,L2 -> Function of the carrier of L1, the carrier of L2 means :Def1: :: LATTICE4:def 1
for a1, b1 being Element of L1 holds
( it . (a1 "\/" b1) = (it . a1) "\/" (it . b1) & it . (a1 "/\" b1) = (it . a1) "/\" (it . b1) );
existence
ex b1 being Function of the carrier of L1, the carrier of L2 st
for a1, b1 being Element of L1 holds
( b1 . (a1 "\/" b1) = (b1 . a1) "\/" (b1 . b1) & b1 . (a1 "/\" b1) = (b1 . a1) "/\" (b1 . b1) )
proof
set b = the Element of L2;
defpred S1[ set , set ] means for a1 being Element of L1 st $1 = a1 holds
$2 = the Element of L2;
A1: now__::_thesis:_for_x_being_Element_of_L1_ex_b_being_Element_of_L2_st_S1[x,b]
let x be Element of L1; ::_thesis: ex b being Element of L2 st S1[x,b]
take b = the Element of L2; ::_thesis: S1[x,b]
thus S1[x,b] ; ::_thesis: verum
end;
consider f being Function of the carrier of L1, the carrier of L2 such that
A2: for x being Element of L1 holds S1[x,f . x] from FUNCT_2:sch_3(A1);
take f ; ::_thesis: for a1, b1 being Element of L1 holds
( f . (a1 "\/" b1) = (f . a1) "\/" (f . b1) & f . (a1 "/\" b1) = (f . a1) "/\" (f . b1) )
now__::_thesis:_for_a1,_b1_being_Element_of_L1_holds_
(_f_._(a1_"\/"_b1)_=_(f_._a1)_"\/"_(f_._b1)_&_f_._(a1_"/\"_b1)_=_(f_._a1)_"/\"_(f_._b1)_)
let a1, b1 be Element of L1; ::_thesis: ( f . (a1 "\/" b1) = (f . a1) "\/" (f . b1) & f . (a1 "/\" b1) = (f . a1) "/\" (f . b1) )
thus f . (a1 "\/" b1) = the Element of L2 by A2
.= the Element of L2 "\/" the Element of L2
.= (f . a1) "\/" the Element of L2 by A2
.= (f . a1) "\/" (f . b1) by A2 ; ::_thesis: f . (a1 "/\" b1) = (f . a1) "/\" (f . b1)
thus f . (a1 "/\" b1) = the Element of L2 by A2
.= the Element of L2 "/\" the Element of L2
.= (f . a1) "/\" the Element of L2 by A2
.= (f . a1) "/\" (f . b1) by A2 ; ::_thesis: verum
end;
hence for a1, b1 being Element of L1 holds
( f . (a1 "\/" b1) = (f . a1) "\/" (f . b1) & f . (a1 "/\" b1) = (f . a1) "/\" (f . b1) ) ; ::_thesis: verum
end;
end;
:: 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 Th4: :: LATTICE4:4
for L1, L2 being Lattice
for a1, b1 being Element of L1
for f being Homomorphism of L1,L2 st a1 [= b1 holds
f . a1 [= f . b1
proof
let L1, L2 be Lattice; ::_thesis: for a1, b1 being Element of L1
for f being Homomorphism of L1,L2 st a1 [= b1 holds
f . a1 [= f . b1
let a1, b1 be Element of L1; ::_thesis: for f being Homomorphism of L1,L2 st a1 [= b1 holds
f . a1 [= f . b1
let f be Homomorphism of L1,L2; ::_thesis: ( a1 [= b1 implies f . a1 [= f . b1 )
assume A1: a1 [= b1 ; ::_thesis: f . a1 [= f . b1
(f . a1) "\/" (f . b1) = f . (a1 "\/" b1) by Def1
.= f . b1 by A1, LATTICES:def_3 ;
hence f . a1 [= f . b1 by LATTICES:def_3; ::_thesis: verum
end;
theorem Th5: :: LATTICE4:5
for L1, L2 being Lattice
for a1, b1 being Element of L1
for f being Homomorphism of L1,L2 st f is one-to-one holds
( a1 [= b1 iff f . a1 [= f . b1 )
proof
let L1, L2 be Lattice; ::_thesis: for a1, b1 being Element of L1
for f being Homomorphism of L1,L2 st f is one-to-one holds
( a1 [= b1 iff f . a1 [= f . b1 )
let a1, b1 be Element of L1; ::_thesis: for f being Homomorphism of L1,L2 st f is one-to-one holds
( a1 [= b1 iff f . a1 [= f . b1 )
let f be Homomorphism of L1,L2; ::_thesis: ( f is one-to-one implies ( a1 [= b1 iff f . a1 [= f . b1 ) )
assume A1: f is one-to-one ; ::_thesis: ( a1 [= b1 iff f . a1 [= f . b1 )
reconsider f = f as Function of the carrier of L1, the carrier of L2 ;
( f . a1 [= f . b1 implies a1 [= b1 )
proof
assume f . a1 [= f . b1 ; ::_thesis: a1 [= b1
then (f . a1) "\/" (f . b1) = f . b1 by LATTICES:def_3;
then f . (a1 "\/" b1) = f . b1 by Def1;
hence a1 "\/" b1 = b1 by A1, FUNCT_2:19; :: according to LATTICES:def_3 ::_thesis: verum
end;
hence ( a1 [= b1 iff f . a1 [= f . b1 ) by Th4; ::_thesis: verum
end;
theorem Th6: :: LATTICE4:6
for L1, L2 being Lattice
for f being Function of the carrier of L1, the carrier of L2 st f is onto holds
for a2 being Element of L2 ex a1 being Element of L1 st a2 = f . a1
proof
let L1, L2 be Lattice; ::_thesis: for f being Function of the carrier of L1, the carrier of L2 st f is onto holds
for a2 being Element of L2 ex a1 being Element of L1 st a2 = f . a1
let f be Function of the carrier of L1, the carrier of L2; ::_thesis: ( f is onto implies for a2 being Element of L2 ex a1 being Element of L1 st a2 = f . a1 )
reconsider g = f as Function of the carrier of L1, the carrier of L2 ;
assume f is onto ; ::_thesis: for a2 being Element of L2 ex a1 being Element of L1 st a2 = f . a1
then A1: rng g = the carrier of L2 by FUNCT_2:def_3;
now__::_thesis:_for_a2_being_Element_of_L2_ex_a1_being_Element_of_L1_st_g_._a1_=_a2
let a2 be Element of L2; ::_thesis: ex a1 being Element of L1 st g . a1 = a2
ex x being set st
( x in the carrier of L1 & g . x = a2 ) by A1, FUNCT_2:11;
hence ex a1 being Element of L1 st g . a1 = a2 ; ::_thesis: verum
end;
hence for a2 being Element of L2 ex a1 being Element of L1 st a2 = f . a1 ; ::_thesis: verum
end;
definition
let L1, L2 be Lattice;
redefine pred L1,L2 are_isomorphic means :: LATTICE4:def 2
ex f being Homomorphism of L1,L2 st f is bijective ;
compatibility
( L1,L2 are_isomorphic iff ex f being Homomorphism of L1,L2 st f is bijective )
proof
thus ( L1,L2 are_isomorphic implies ex f being Homomorphism of L1,L2 st f is bijective ) ::_thesis: ( ex f being Homomorphism of L1,L2 st f is bijective implies L1,L2 are_isomorphic )
proof
set R = LattRel L1;
set S = LattRel L2;
assume L1,L2 are_isomorphic ; ::_thesis: ex f being Homomorphism of L1,L2 st f is bijective
then LattRel L1, LattRel L2 are_isomorphic by FILTER_1:def_9;
then consider F being Function such that
A1: F is_isomorphism_of LattRel L1, LattRel L2 by WELLORD1:def_8;
A2: dom F = field (LattRel L1) by A1, WELLORD1:def_7;
A3: ( field (LattRel L2) = the carrier of L2 & rng F = field (LattRel L2) ) by A1, FILTER_1:32, WELLORD1:def_7;
A4: field (LattRel L1) = the carrier of L1 by FILTER_1:32;
then reconsider F = F as Function of the carrier of L1, the carrier of L2 by A2, A3, FUNCT_2:1;
now__::_thesis:_for_a1,_b1_being_Element_of_L1_holds_
(_F_._(a1_"\/"_b1)_=_(F_._a1)_"\/"_(F_._b1)_&_F_._(a1_"/\"_b1)_=_(F_._a1)_"/\"_(F_._b1)_)
let a1, b1 be Element of L1; ::_thesis: ( F . (a1 "\/" b1) = (F . a1) "\/" (F . b1) & F . (a1 "/\" b1) = (F . a1) "/\" (F . b1) )
reconsider a19 = a1, b19 = b1 as Element of L1 ;
A5: F is onto by A3, FUNCT_2:def_3;
thus F . (a1 "\/" b1) = (F . a1) "\/" (F . b1) ::_thesis: F . (a1 "/\" b1) = (F . a1) "/\" (F . b1)
proof
b19 [= a19 "\/" b19 by LATTICES:5;
then [b1,(a1 "\/" b1)] in LattRel L1 by FILTER_1:31;
then [(F . b1),(F . (a1 "\/" b1))] in LattRel L2 by A1, WELLORD1:def_7;
then A6: F . b19 [= F . (a19 "\/" b19) by FILTER_1:31;
consider k1 being Element of L1 such that
A7: (F . a1) "\/" (F . b1) = F . k1 by A5, Th6;
F . b1 [= F . k1 by A7, LATTICES:5;
then [(F . b1),(F . k1)] in LattRel L2 by FILTER_1:31;
then [b1,k1] in LattRel L1 by A1, A4, WELLORD1:def_7;
then A8: b1 [= k1 by FILTER_1:31;
F . a1 [= F . k1 by A7, LATTICES:5;
then [(F . a1),(F . k1)] in LattRel L2 by FILTER_1:31;
then [a1,k1] in LattRel L1 by A1, A4, WELLORD1:def_7;
then a1 [= k1 by FILTER_1:31;
then a1 "\/" b1 [= k1 by A8, FILTER_0:6;
then [(a1 "\/" b1),k1] in LattRel L1 by FILTER_1:31;
then [(F . (a1 "\/" b1)),(F . k1)] in LattRel L2 by A1, WELLORD1:def_7;
then A9: F . (a1 "\/" b1) [= (F . a1) "\/" (F . b1) by A7, FILTER_1:31;
a19 [= a19 "\/" b19 by LATTICES:5;
then [a1,(a1 "\/" b1)] in LattRel L1 by FILTER_1:31;
then [(F . a1),(F . (a1 "\/" b1))] in LattRel L2 by A1, WELLORD1:def_7;
then F . a19 [= F . (a19 "\/" b19) by FILTER_1:31;
then (F . a1) "\/" (F . b1) [= F . (a1 "\/" b1) by A6, FILTER_0:6;
hence F . (a1 "\/" b1) = (F . a1) "\/" (F . b1) by A9, LATTICES:8; ::_thesis: verum
end;
thus F . (a1 "/\" b1) = (F . a1) "/\" (F . b1) ::_thesis: verum
proof
a19 "/\" b19 [= b19 by LATTICES:6;
then [(a1 "/\" b1),b1] in LattRel L1 by FILTER_1:31;
then [(F . (a1 "/\" b1)),(F . b1)] in LattRel L2 by A1, WELLORD1:def_7;
then A10: F . (a19 "/\" b19) [= F . b19 by FILTER_1:31;
consider k1 being Element of L1 such that
A11: (F . a1) "/\" (F . b1) = F . k1 by A5, Th6;
F . k1 [= F . b1 by A11, LATTICES:6;
then [(F . k1),(F . b1)] in LattRel L2 by FILTER_1:31;
then [k1,b1] in LattRel L1 by A1, A4, WELLORD1:def_7;
then A12: k1 [= b1 by FILTER_1:31;
F . k1 [= F . a1 by A11, LATTICES:6;
then [(F . k1),(F . a1)] in LattRel L2 by FILTER_1:31;
then [k1,a1] in LattRel L1 by A1, A4, WELLORD1:def_7;
then k1 [= a1 by FILTER_1:31;
then k1 [= a1 "/\" b1 by A12, FILTER_0:7;
then [k1,(a1 "/\" b1)] in LattRel L1 by FILTER_1:31;
then [(F . k1),(F . (a1 "/\" b1))] in LattRel L2 by A1, WELLORD1:def_7;
then A13: (F . a1) "/\" (F . b1) [= F . (a1 "/\" b1) by A11, FILTER_1:31;
a19 "/\" b19 [= a19 by LATTICES:6;
then [(a1 "/\" b1),a1] in LattRel L1 by FILTER_1:31;
then [(F . (a1 "/\" b1)),(F . a1)] in LattRel L2 by A1, WELLORD1:def_7;
then F . (a19 "/\" b19) [= F . a19 by FILTER_1:31;
then F . (a1 "/\" b1) [= (F . a1) "/\" (F . b1) by A10, FILTER_0:7;
hence F . (a1 "/\" b1) = (F . a1) "/\" (F . b1) by A13, LATTICES:8; ::_thesis: verum
end;
end;
then reconsider F = F as Homomorphism of L1,L2 by Def1;
take F ; ::_thesis: F is bijective
( F is one-to-one & F is onto ) by A1, A3, FUNCT_2:def_3, WELLORD1:def_7;
hence F is bijective ; ::_thesis: verum
end;
set R = LattRel L1;
set S = LattRel L2;
given f being Homomorphism of L1,L2 such that A14: f is bijective ; ::_thesis: L1,L2 are_isomorphic
A15: for a, b being set holds
( [a,b] in LattRel L1 iff ( a in field (LattRel L1) & b in field (LattRel L1) & [(f . a),(f . b)] in LattRel L2 ) )
proof
let a, b be set ; ::_thesis: ( [a,b] in LattRel L1 iff ( a in field (LattRel L1) & b in field (LattRel L1) & [(f . a),(f . b)] in LattRel L2 ) )
hereby ::_thesis: ( a in field (LattRel L1) & b in field (LattRel L1) & [(f . a),(f . b)] in LattRel L2 implies [a,b] in LattRel L1 )
assume A16: [a,b] in LattRel L1 ; ::_thesis: ( a in field (LattRel L1) & b in field (LattRel L1) & [(f . a),(f . b)] in LattRel L2 )
hence ( a in field (LattRel L1) & b in field (LattRel L1) ) by RELAT_1:15; ::_thesis: [(f . a),(f . b)] in LattRel L2
then reconsider a9 = a, b9 = b as Element of L1 by FILTER_1:32;
a9 [= b9 by A16, FILTER_1:31;
then f . a9 [= f . b9 by A14, Th5;
hence [(f . a),(f . b)] in LattRel L2 by FILTER_1:31; ::_thesis: verum
end;
assume that
A17: ( a in field (LattRel L1) & b in field (LattRel L1) ) and
A18: [(f . a),(f . b)] in LattRel L2 ; ::_thesis: [a,b] in LattRel L1
reconsider a9 = a, b9 = b as Element of L1 by A17, FILTER_1:32;
f . a9 [= f . b9 by A18, FILTER_1:31;
then a9 [= b9 by A14, Th5;
hence [a,b] in LattRel L1 by FILTER_1:31; ::_thesis: verum
end;
A19: dom f = the carrier of L1 by FUNCT_2:def_1
.= field (LattRel L1) by FILTER_1:32 ;
rng f = the carrier of L2 by A14, FUNCT_2:def_3
.= field (LattRel L2) by FILTER_1:32 ;
then f is_isomorphism_of LattRel L1, LattRel L2 by A14, A19, A15, WELLORD1:def_7;
then LattRel L1, LattRel L2 are_isomorphic by WELLORD1:def_8;
hence L1,L2 are_isomorphic by FILTER_1:def_9; ::_thesis: verum
end;
end;
:: deftheorem defines are_isomorphic LATTICE4:def_2_:_
for L1, L2 being Lattice holds
( L1,L2 are_isomorphic iff ex f being Homomorphism of L1,L2 st f is bijective );
definition
let L1, L2 be Lattice;
let f be Homomorphism of L1,L2;
predf preserves_implication means :Def3: :: LATTICE4:def 3
for a1, b1 being Element of L1 holds f . (a1 => b1) = (f . a1) => (f . b1);
predf preserves_top means :Def4: :: LATTICE4:def 4
f . (Top L1) = Top L2;
predf preserves_bottom means :Def5: :: LATTICE4:def 5
f . (Bottom L1) = Bottom L2;
predf preserves_complement means :Def6: :: LATTICE4:def 6
for a1 being Element of L1 holds f . (a1 `) = (f . a1) ` ;
end;
:: deftheorem Def3 defines preserves_implication LATTICE4:def_3_:_
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 Def4 defines preserves_top LATTICE4:def_4_:_
for L1, L2 being Lattice
for f being Homomorphism of L1,L2 holds
( f preserves_top iff f . (Top L1) = Top L2 );
:: deftheorem Def5 defines preserves_bottom LATTICE4:def_5_:_
for L1, L2 being Lattice
for f being Homomorphism of L1,L2 holds
( f preserves_bottom iff f . (Bottom L1) = Bottom L2 );
:: deftheorem Def6 defines preserves_complement LATTICE4:def_6_:_
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) ` );
definition
let L be Lattice;
mode ClosedSubset of L is meet-closed join-closed Subset of L;
end;
theorem Th7: :: LATTICE4:7
for L being Lattice holds the carrier of L is ClosedSubset of L
proof
let L be Lattice; ::_thesis: the carrier of L is ClosedSubset of L
the carrier of L c= the carrier of L ;
then reconsider F = the carrier of L as Subset of L ;
A1: for p, q being Element of L st p in F & q in F holds
p "/\" q in F ;
for p, q being Element of L st p in F & q in F holds
p "\/" q in F ;
hence the carrier of L is ClosedSubset of L by A1, LATTICES:def_24, LATTICES:def_25; ::_thesis: verum
end;
registration
let L be Lattice;
cluster non empty meet-closed join-closed for Element of bool the carrier of L;
existence
not for b1 being ClosedSubset of L holds b1 is empty
proof
the carrier of L is ClosedSubset of L by Th7;
hence not for b1 being ClosedSubset of L holds b1 is empty ; ::_thesis: verum
end;
end;
theorem :: LATTICE4:8
for L being Lattice
for F being Filter of L holds F is ClosedSubset of L ;
definition
let L be Lattice;
let B be Finite_Subset of the carrier of L;
func FinJoin B -> Element of L equals :: LATTICE4:def 7
FinJoin (B,(id L));
coherence
FinJoin (B,(id L)) is Element of L ;
func FinMeet B -> Element of L equals :: LATTICE4:def 8
FinMeet (B,(id L));
coherence
FinMeet (B,(id L)) is Element of L ;
end;
:: deftheorem defines FinJoin LATTICE4:def_7_:_
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_8_:_
for L being Lattice
for B being Finite_Subset of the carrier of L holds FinMeet B = FinMeet (B,(id L));
theorem Th9: :: LATTICE4:9
for L being Lattice
for p being Element of L holds FinJoin {.p.} = p
proof
let L be Lattice; ::_thesis: for p being Element of L holds FinJoin {.p.} = p
let p be Element of L; ::_thesis: FinJoin {.p.} = p
thus FinJoin {.p.} = the L_join of L $$ ({.p.},(id L)) by LATTICE2:def_3
.= (id L) . p by SETWISEO:17
.= p by FUNCT_1:18 ; ::_thesis: verum
end;
theorem Th10: :: LATTICE4:10
for L being Lattice
for p being Element of L holds FinMeet {.p.} = p
proof
let L be Lattice; ::_thesis: for p being Element of L holds FinMeet {.p.} = p
let p be Element of L; ::_thesis: FinMeet {.p.} = p
set M = the L_meet of L;
thus FinMeet {.p.} = the L_meet of L $$ ({.p.},(id L)) by LATTICE2:def_4
.= (id L) . p by SETWISEO:17
.= p by FUNCT_1:18 ; ::_thesis: verum
end;
begin
theorem Th11: :: LATTICE4:11
for L2 being Lattice
for DL being distributive Lattice
for f being Homomorphism of DL,L2 st f is onto holds
L2 is distributive
proof
let L2 be Lattice; ::_thesis: for DL being distributive Lattice
for f being Homomorphism of DL,L2 st f is onto holds
L2 is distributive
let DL be distributive Lattice; ::_thesis: for f being Homomorphism of DL,L2 st f is onto holds
L2 is distributive
let f be Homomorphism of DL,L2; ::_thesis: ( f is onto implies L2 is distributive )
assume A1: f is onto ; ::_thesis: L2 is distributive
thus L2 is distributive ::_thesis: verum
proof
let a, b, c be Element of L2; :: according to LATTICES:def_11 ::_thesis: a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)
consider a9 being Element of DL such that
A2: f . a9 = a by A1, Th6;
consider c9 being Element of DL such that
A3: f . c9 = c by A1, Th6;
consider b9 being Element of DL such that
A4: f . b9 = b by A1, Th6;
thus a "/\" (b "\/" c) = a "/\" (f . (b9 "\/" c9)) by A4, A3, Def1
.= f . (a9 "/\" (b9 "\/" c9)) by A2, Def1
.= f . ((a9 "/\" b9) "\/" (a9 "/\" c9)) by LATTICES:def_11
.= (f . (a9 "/\" b9)) "\/" (f . (a9 "/\" c9)) by Def1
.= (a "/\" b) "\/" (f . (a9 "/\" c9)) by A2, A4, Def1
.= (a "/\" b) "\/" (a "/\" c) by A2, A3, Def1 ; ::_thesis: verum
end;
end;
begin
theorem Th12: :: LATTICE4:12
for L2 being Lattice
for 0L being lower-bounded Lattice
for f being Homomorphism of 0L,L2 st f is onto holds
( L2 is lower-bounded & f preserves_bottom )
proof
let L2 be Lattice; ::_thesis: for 0L being lower-bounded Lattice
for f being Homomorphism of 0L,L2 st f is onto holds
( L2 is lower-bounded & f preserves_bottom )
let 0L be lower-bounded Lattice; ::_thesis: for f being Homomorphism of 0L,L2 st f is onto holds
( L2 is lower-bounded & f preserves_bottom )
let f be Homomorphism of 0L,L2; ::_thesis: ( f is onto implies ( L2 is lower-bounded & f preserves_bottom ) )
set r = f . (Bottom 0L);
assume A1: f is onto ; ::_thesis: ( L2 is lower-bounded & f preserves_bottom )
A2: now__::_thesis:_for_a2_being_Element_of_L2_holds_
(_(f_._(Bottom_0L))_"/\"_a2_=_f_._(Bottom_0L)_&_a2_"/\"_(f_._(Bottom_0L))_=_f_._(Bottom_0L)_)
let a2 be Element of L2; ::_thesis: ( (f . (Bottom 0L)) "/\" a2 = f . (Bottom 0L) & a2 "/\" (f . (Bottom 0L)) = f . (Bottom 0L) )
consider a1 being Element of 0L such that
A3: f . a1 = a2 by A1, Th6;
thus (f . (Bottom 0L)) "/\" a2 = f . ((Bottom 0L) "/\" a1) by A3, Def1
.= f . (Bottom 0L) by LATTICES:15 ; ::_thesis: a2 "/\" (f . (Bottom 0L)) = f . (Bottom 0L)
hence a2 "/\" (f . (Bottom 0L)) = f . (Bottom 0L) ; ::_thesis: verum
end;
thus L2 is lower-bounded ::_thesis: f preserves_bottom
proof
take f . (Bottom 0L) ; :: according to LATTICES:def_13 ::_thesis: for b1 being Element of the carrier of L2 holds
( (f . (Bottom 0L)) "/\" b1 = f . (Bottom 0L) & b1 "/\" (f . (Bottom 0L)) = f . (Bottom 0L) )
thus for b1 being Element of the carrier of L2 holds
( (f . (Bottom 0L)) "/\" b1 = f . (Bottom 0L) & b1 "/\" (f . (Bottom 0L)) = f . (Bottom 0L) ) by A2; ::_thesis: verum
end;
then Bottom L2 = f . (Bottom 0L) by A2, LATTICES:def_16;
hence f preserves_bottom by Def5; ::_thesis: verum
end;
theorem Th13: :: LATTICE4:13
for 0L being lower-bounded Lattice
for B being Finite_Subset of the carrier of 0L
for b being Element of 0L
for f being UnOp of the carrier of 0L holds FinJoin ((B \/ {.b.}),f) = (FinJoin (B,f)) "\/" (f . b)
proof
let 0L be lower-bounded Lattice; ::_thesis: for B being Finite_Subset of the carrier of 0L
for b being Element of 0L
for f being UnOp of the carrier of 0L holds FinJoin ((B \/ {.b.}),f) = (FinJoin (B,f)) "\/" (f . b)
let B be Finite_Subset of the carrier of 0L; ::_thesis: for b being Element of 0L
for f being UnOp of the carrier of 0L holds FinJoin ((B \/ {.b.}),f) = (FinJoin (B,f)) "\/" (f . b)
let b be Element of 0L; ::_thesis: for f being UnOp of the carrier of 0L holds FinJoin ((B \/ {.b.}),f) = (FinJoin (B,f)) "\/" (f . b)
let f be UnOp of the carrier of 0L; ::_thesis: FinJoin ((B \/ {.b.}),f) = (FinJoin (B,f)) "\/" (f . b)
set J = the L_join of 0L;
thus FinJoin ((B \/ {.b.}),f) = the L_join of 0L $$ ((B \/ {.b.}),f) by LATTICE2:def_3
.= ( the L_join of 0L $$ (B,f)) "\/" (f . b) by SETWISEO:32
.= (FinJoin (B,f)) "\/" (f . b) by LATTICE2:def_3 ; ::_thesis: verum
end;
theorem Th14: :: LATTICE4:14
for 0L being lower-bounded Lattice
for B being Finite_Subset of the carrier of 0L
for b being Element of 0L holds FinJoin (B \/ {.b.}) = (FinJoin B) "\/" b
proof
let 0L be lower-bounded Lattice; ::_thesis: for B being Finite_Subset of the carrier of 0L
for b being Element of 0L holds FinJoin (B \/ {.b.}) = (FinJoin B) "\/" b
let B be Finite_Subset of the carrier of 0L; ::_thesis: for b being Element of 0L holds FinJoin (B \/ {.b.}) = (FinJoin B) "\/" b
let b be Element of 0L; ::_thesis: FinJoin (B \/ {.b.}) = (FinJoin B) "\/" b
thus FinJoin (B \/ {.b.}) = (FinJoin (B,(id 0L))) "\/" ((id 0L) . b) by Th13
.= (FinJoin B) "\/" b by FUNCT_1:18 ; ::_thesis: verum
end;
theorem :: LATTICE4:15
for 0L being lower-bounded Lattice
for B1, B2 being Finite_Subset of the carrier of 0L holds (FinJoin B1) "\/" (FinJoin B2) = FinJoin (B1 \/ B2)
proof
let 0L be lower-bounded Lattice; ::_thesis: for B1, B2 being Finite_Subset of the carrier of 0L holds (FinJoin B1) "\/" (FinJoin B2) = FinJoin (B1 \/ B2)
let B1, B2 be Finite_Subset of the carrier of 0L; ::_thesis: (FinJoin B1) "\/" (FinJoin B2) = FinJoin (B1 \/ B2)
set J = the L_join of 0L;
thus FinJoin (B1 \/ B2) = the L_join of 0L $$ ((B1 \/ B2),(id 0L)) by LATTICE2:def_3
.= ( the L_join of 0L $$ (B1,(id 0L))) "\/" ( the L_join of 0L $$ (B2,(id 0L))) by SETWISEO:33
.= (FinJoin B1) "\/" ( the L_join of 0L $$ (B2,(id 0L))) by LATTICE2:def_3
.= (FinJoin B1) "\/" (FinJoin B2) by LATTICE2:def_3 ; ::_thesis: verum
end;
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
proof
let 0L be lower-bounded Lattice; ::_thesis: for f being Function of the carrier of 0L, the carrier of 0L holds FinJoin (({}. the carrier of 0L),f) = Bottom 0L
let f be Function of the carrier of 0L, the carrier of 0L; ::_thesis: FinJoin (({}. the carrier of 0L),f) = Bottom 0L
set J = the L_join of 0L;
thus FinJoin (({}. the carrier of 0L),f) = the L_join of 0L $$ (({}. the carrier of 0L),f) by LATTICE2:def_3
.= the_unity_wrt the L_join of 0L by SETWISEO:31
.= Bottom 0L by LATTICE2:52 ; ::_thesis: verum
end;
theorem :: LATTICE4:16
for 0L being lower-bounded Lattice holds FinJoin ({}. the carrier of 0L) = Bottom 0L by Lm1;
theorem Th17: :: LATTICE4:17
for 0L being lower-bounded Lattice
for A being ClosedSubset of 0L st Bottom 0L in A holds
for B being Finite_Subset of the carrier of 0L st B c= A holds
FinJoin B in A
proof
let 0L be lower-bounded Lattice; ::_thesis: for A being ClosedSubset of 0L st Bottom 0L in A holds
for B being Finite_Subset of the carrier of 0L st B c= A holds
FinJoin B in A
let A be ClosedSubset of 0L; ::_thesis: ( Bottom 0L in A implies for B being Finite_Subset of the carrier of 0L st B c= A holds
FinJoin B in A )
defpred S1[ Finite_Subset of the carrier of 0L] means ( $1 c= A implies FinJoin $1 in A );
A1: for B1 being Finite_Subset of the carrier of 0L
for p being Element of 0L st S1[B1] holds
S1[B1 \/ {.p.}]
proof
let B1 be Finite_Subset of the carrier of 0L; ::_thesis: for p being Element of 0L st S1[B1] holds
S1[B1 \/ {.p.}]
let p be Element of 0L; ::_thesis: ( S1[B1] implies S1[B1 \/ {.p.}] )
assume A2: ( B1 c= A implies FinJoin B1 in A ) ; ::_thesis: S1[B1 \/ {.p.}]
assume A3: B1 \/ {p} c= A ; ::_thesis: FinJoin (B1 \/ {.p.}) in A
then {p} c= A by XBOOLE_1:11;
then p in A by ZFMISC_1:31;
then (FinJoin B1) "\/" p in A by A2, A3, LATTICES:def_25, XBOOLE_1:11;
hence FinJoin (B1 \/ {.p.}) in A by Th14; ::_thesis: verum
end;
assume Bottom 0L in A ; ::_thesis: for B being Finite_Subset of the carrier of 0L st B c= A holds
FinJoin B in A
then A4: S1[ {}. the carrier of 0L] by Lm1;
thus for B being Element of Fin the carrier of 0L holds S1[B] from SETWISEO:sch_4(A4, A1); ::_thesis: verum
end;
begin
theorem Th18: :: LATTICE4:18
for L2 being Lattice
for 1L being upper-bounded Lattice
for f being Homomorphism of 1L,L2 st f is onto holds
( L2 is upper-bounded & f preserves_top )
proof
let L2 be Lattice; ::_thesis: for 1L being upper-bounded Lattice
for f being Homomorphism of 1L,L2 st f is onto holds
( L2 is upper-bounded & f preserves_top )
let 1L be upper-bounded Lattice; ::_thesis: for f being Homomorphism of 1L,L2 st f is onto holds
( L2 is upper-bounded & f preserves_top )
let f be Homomorphism of 1L,L2; ::_thesis: ( f is onto implies ( L2 is upper-bounded & f preserves_top ) )
set r = f . (Top 1L);
assume A1: f is onto ; ::_thesis: ( L2 is upper-bounded & f preserves_top )
A2: now__::_thesis:_for_a2_being_Element_of_L2_holds_
(_(f_._(Top_1L))_"\/"_a2_=_f_._(Top_1L)_&_a2_"\/"_(f_._(Top_1L))_=_f_._(Top_1L)_)
let a2 be Element of L2; ::_thesis: ( (f . (Top 1L)) "\/" a2 = f . (Top 1L) & a2 "\/" (f . (Top 1L)) = f . (Top 1L) )
consider a1 being Element of 1L such that
A3: f . a1 = a2 by A1, Th6;
thus (f . (Top 1L)) "\/" a2 = f . ((Top 1L) "\/" a1) by A3, Def1
.= f . (Top 1L) by LATTICES:18 ; ::_thesis: a2 "\/" (f . (Top 1L)) = f . (Top 1L)
hence a2 "\/" (f . (Top 1L)) = f . (Top 1L) ; ::_thesis: verum
end;
thus L2 is upper-bounded ::_thesis: f preserves_top
proof
take f . (Top 1L) ; :: according to LATTICES:def_14 ::_thesis: for b1 being Element of the carrier of L2 holds
( (f . (Top 1L)) "\/" b1 = f . (Top 1L) & b1 "\/" (f . (Top 1L)) = f . (Top 1L) )
thus for b1 being Element of the carrier of L2 holds
( (f . (Top 1L)) "\/" b1 = f . (Top 1L) & b1 "\/" (f . (Top 1L)) = f . (Top 1L) ) by A2; ::_thesis: verum
end;
then Top L2 = f . (Top 1L) by A2, LATTICES:def_17;
hence f preserves_top by Def4; ::_thesis: verum
end;
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
proof
let 1L be upper-bounded Lattice; ::_thesis: for f being Function of the carrier of 1L, the carrier of 1L holds FinMeet (({}. the carrier of 1L),f) = Top 1L
let f be Function of the carrier of 1L, the carrier of 1L; ::_thesis: FinMeet (({}. the carrier of 1L),f) = Top 1L
set M = the L_meet of 1L;
thus FinMeet (({}. the carrier of 1L),f) = the L_meet of 1L $$ (({}. the carrier of 1L),f) by LATTICE2:def_4
.= the_unity_wrt the L_meet of 1L by SETWISEO:31
.= Top 1L by LATTICE2:57 ; ::_thesis: verum
end;
theorem :: LATTICE4:19
for 1L being upper-bounded Lattice holds FinMeet ({}. the carrier of 1L) = Top 1L by Lm2;
theorem Th20: :: LATTICE4:20
for 1L being upper-bounded Lattice
for B being Finite_Subset of the carrier of 1L
for b being Element of 1L
for f being UnOp of the carrier of 1L holds FinMeet ((B \/ {.b.}),f) = (FinMeet (B,f)) "/\" (f . b)
proof
let 1L be upper-bounded Lattice; ::_thesis: for B being Finite_Subset of the carrier of 1L
for b being Element of 1L
for f being UnOp of the carrier of 1L holds FinMeet ((B \/ {.b.}),f) = (FinMeet (B,f)) "/\" (f . b)
let B be Finite_Subset of the carrier of 1L; ::_thesis: for b being Element of 1L
for f being UnOp of the carrier of 1L holds FinMeet ((B \/ {.b.}),f) = (FinMeet (B,f)) "/\" (f . b)
let b be Element of 1L; ::_thesis: for f being UnOp of the carrier of 1L holds FinMeet ((B \/ {.b.}),f) = (FinMeet (B,f)) "/\" (f . b)
let f be UnOp of the carrier of 1L; ::_thesis: FinMeet ((B \/ {.b.}),f) = (FinMeet (B,f)) "/\" (f . b)
set M = the L_meet of 1L;
thus FinMeet ((B \/ {.b.}),f) = the L_meet of 1L $$ ((B \/ {.b.}),f) by LATTICE2:def_4
.= ( the L_meet of 1L $$ (B,f)) "/\" (f . b) by SETWISEO:32
.= (FinMeet (B,f)) "/\" (f . b) by LATTICE2:def_4 ; ::_thesis: verum
end;
theorem Th21: :: LATTICE4:21
for 1L being upper-bounded Lattice
for B being Finite_Subset of the carrier of 1L
for b being Element of 1L holds FinMeet (B \/ {.b.}) = (FinMeet B) "/\" b
proof
let 1L be upper-bounded Lattice; ::_thesis: for B being Finite_Subset of the carrier of 1L
for b being Element of 1L holds FinMeet (B \/ {.b.}) = (FinMeet B) "/\" b
let B be Finite_Subset of the carrier of 1L; ::_thesis: for b being Element of 1L holds FinMeet (B \/ {.b.}) = (FinMeet B) "/\" b
let b be Element of 1L; ::_thesis: FinMeet (B \/ {.b.}) = (FinMeet B) "/\" b
thus FinMeet (B \/ {.b.}) = (FinMeet (B,(id 1L))) "/\" ((id 1L) . b) by Th20
.= (FinMeet B) "/\" b by FUNCT_1:18 ; ::_thesis: verum
end;
theorem Th22: :: LATTICE4:22
for 1L being upper-bounded Lattice
for B being Finite_Subset of the carrier of 1L
for f, g being UnOp of the carrier of 1L holds FinMeet ((f .: B),g) = FinMeet (B,(g * f))
proof
let 1L be upper-bounded Lattice; ::_thesis: for B being Finite_Subset of the carrier of 1L
for f, g being UnOp of the carrier of 1L holds FinMeet ((f .: B),g) = FinMeet (B,(g * f))
let B be Finite_Subset of the carrier of 1L; ::_thesis: for f, g being UnOp of the carrier of 1L holds FinMeet ((f .: B),g) = FinMeet (B,(g * f))
let f, g be UnOp of the carrier of 1L; ::_thesis: FinMeet ((f .: B),g) = FinMeet (B,(g * f))
set M = the L_meet of 1L;
thus FinMeet ((f .: B),g) = the L_meet of 1L $$ ((f .: B),g) by LATTICE2:def_4
.= the L_meet of 1L $$ (B,(g * f)) by SETWISEO:35
.= FinMeet (B,(g * f)) by LATTICE2:def_4 ; ::_thesis: verum
end;
theorem Th23: :: LATTICE4:23
for 1L being upper-bounded Lattice
for B1, B2 being Finite_Subset of the carrier of 1L holds (FinMeet B1) "/\" (FinMeet B2) = FinMeet (B1 \/ B2)
proof
let 1L be upper-bounded Lattice; ::_thesis: for B1, B2 being Finite_Subset of the carrier of 1L holds (FinMeet B1) "/\" (FinMeet B2) = FinMeet (B1 \/ B2)
let B1, B2 be Finite_Subset of the carrier of 1L; ::_thesis: (FinMeet B1) "/\" (FinMeet B2) = FinMeet (B1 \/ B2)
set M = the L_meet of 1L;
thus FinMeet (B1 \/ B2) = the L_meet of 1L $$ ((B1 \/ B2),(id 1L)) by LATTICE2:def_4
.= ( the L_meet of 1L $$ (B1,(id 1L))) "/\" ( the L_meet of 1L $$ (B2,(id 1L))) by SETWISEO:33
.= (FinMeet B1) "/\" ( the L_meet of 1L $$ (B2,(id 1L))) by LATTICE2:def_4
.= (FinMeet B1) "/\" (FinMeet B2) by LATTICE2:def_4 ; ::_thesis: verum
end;
theorem Th24: :: LATTICE4:24
for 1L being upper-bounded Lattice
for F being ClosedSubset of 1L st Top 1L in F holds
for B being Finite_Subset of the carrier of 1L st B c= F holds
FinMeet B in F
proof
let 1L be upper-bounded Lattice; ::_thesis: for F being ClosedSubset of 1L st Top 1L in F holds
for B being Finite_Subset of the carrier of 1L st B c= F holds
FinMeet B in F
let F be ClosedSubset of 1L; ::_thesis: ( Top 1L in F implies for B being Finite_Subset of the carrier of 1L st B c= F holds
FinMeet B in F )
defpred S1[ Finite_Subset of the carrier of 1L] means ( $1 c= F implies FinMeet $1 in F );
A1: for B1 being Finite_Subset of the carrier of 1L
for p being Element of 1L st S1[B1] holds
S1[B1 \/ {.p.}]
proof
let B1 be Finite_Subset of the carrier of 1L; ::_thesis: for p being Element of 1L st S1[B1] holds
S1[B1 \/ {.p.}]
let p be Element of 1L; ::_thesis: ( S1[B1] implies S1[B1 \/ {.p.}] )
assume A2: ( B1 c= F implies FinMeet B1 in F ) ; ::_thesis: S1[B1 \/ {.p.}]
assume A3: B1 \/ {p} c= F ; ::_thesis: FinMeet (B1 \/ {.p.}) in F
then {p} c= F by XBOOLE_1:11;
then p in F by ZFMISC_1:31;
then (FinMeet B1) "/\" p in F by A2, A3, LATTICES:def_24, XBOOLE_1:11;
hence FinMeet (B1 \/ {.p.}) in F by Th21; ::_thesis: verum
end;
assume Top 1L in F ; ::_thesis: for B being Finite_Subset of the carrier of 1L st B c= F holds
FinMeet B in F
then A4: S1[ {}. the carrier of 1L] by Lm2;
thus for B being Element of Fin the carrier of 1L holds S1[B] from SETWISEO:sch_4(A4, A1); ::_thesis: verum
end;
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)))
proof
let DL be distributive upper-bounded Lattice; ::_thesis: 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)))
let B be Finite_Subset of the carrier of DL; ::_thesis: 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)))
let p be Element of DL; ::_thesis: 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)))
let f be UnOp of the carrier of DL; ::_thesis: 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)))
set J = the L_join of DL;
set M = the L_meet of DL;
now__::_thesis:_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)))
percases ( B <> {} or B = {} ) ;
suppose B <> {} ; ::_thesis: 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)))
hence 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))) by LATTICE2:21, SETWISEO:28; ::_thesis: verum
end;
supposeA1: B = {} ; ::_thesis: 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)))
A2: now__::_thesis:_for_f_being_UnOp_of_the_carrier_of_DL_holds_the_L_meet_of_DL_$$_(B,f)_=_Top_DL
let f be UnOp of the carrier of DL; ::_thesis: the L_meet of DL $$ (B,f) = Top DL
thus the L_meet of DL $$ (B,f) = FinMeet (({}. the carrier of DL),f) by A1, LATTICE2:def_4
.= Top DL by Lm2 ; ::_thesis: verum
end;
hence the L_join of DL . (( the L_meet of DL $$ (B,f)),p) = (Top DL) "\/" p
.= Top DL
.= the L_meet of DL $$ (B,( the L_join of DL [:] (f,p))) by A2 ;
::_thesis: verum
end;
end;
end;
hence 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))) ; ::_thesis: verum
end;
theorem Th25: :: LATTICE4:25
for DL being distributive upper-bounded Lattice
for B being Finite_Subset of the carrier of DL
for p being Element of DL holds (FinMeet B) "\/" p = FinMeet (( the L_join of DL [:] ((id DL),p)) .: B)
proof
let DL be distributive upper-bounded Lattice; ::_thesis: for B being Finite_Subset of the carrier of DL
for p being Element of DL holds (FinMeet B) "\/" p = FinMeet (( the L_join of DL [:] ((id DL),p)) .: B)
let B be Finite_Subset of the carrier of DL; ::_thesis: for p being Element of DL holds (FinMeet B) "\/" p = FinMeet (( the L_join of DL [:] ((id DL),p)) .: B)
let p be Element of DL; ::_thesis: (FinMeet B) "\/" p = FinMeet (( the L_join of DL [:] ((id DL),p)) .: B)
set J = the L_join of DL;
set M = the L_meet of DL;
thus (FinMeet B) "\/" p = the L_join of DL . (( the L_meet of DL $$ (B,(id DL))),p) by LATTICE2:def_4
.= the L_meet of DL $$ (B,( the L_join of DL [:] ((id DL),p))) by Lm3
.= FinMeet (B,( the L_join of DL [:] ((id DL),p))) by LATTICE2:def_4
.= FinMeet (B,((id DL) * ( the L_join of DL [:] ((id DL),p)))) by FUNCT_2:17
.= FinMeet (( the L_join of DL [:] ((id DL),p)) .: B) by Th22 ; ::_thesis: verum
end;
begin
theorem Th26: :: LATTICE4:26
for CL being C_Lattice
for IL being implicative Lattice
for f being Homomorphism of IL,CL
for i, j being Element of IL holds (f . i) "/\" (f . (i => j)) [= f . j
proof
let CL be C_Lattice; ::_thesis: for IL being implicative Lattice
for f being Homomorphism of IL,CL
for i, j being Element of IL holds (f . i) "/\" (f . (i => j)) [= f . j
let IL be implicative Lattice; ::_thesis: for f being Homomorphism of IL,CL
for i, j being Element of IL holds (f . i) "/\" (f . (i => j)) [= f . j
let f be Homomorphism of IL,CL; ::_thesis: for i, j being Element of IL holds (f . i) "/\" (f . (i => j)) [= f . j
let i, j be Element of IL; ::_thesis: (f . i) "/\" (f . (i => j)) [= f . j
i "/\" (i => j) [= j by FILTER_0:def_7;
then f . (i "/\" (i => j)) [= f . j by Th4;
hence (f . i) "/\" (f . (i => j)) [= f . j by Def1; ::_thesis: verum
end;
theorem Th27: :: LATTICE4:27
for CL being C_Lattice
for IL being implicative Lattice
for f being Homomorphism of IL,CL
for i, k, j being Element of IL st f is one-to-one & (f . i) "/\" (f . k) [= f . j holds
f . k [= f . (i => j)
proof
let CL be C_Lattice; ::_thesis: for IL being implicative Lattice
for f being Homomorphism of IL,CL
for i, k, j being Element of IL st f is one-to-one & (f . i) "/\" (f . k) [= f . j holds
f . k [= f . (i => j)
let IL be implicative Lattice; ::_thesis: for f being Homomorphism of IL,CL
for i, k, j being Element of IL st f is one-to-one & (f . i) "/\" (f . k) [= f . j holds
f . k [= f . (i => j)
let f be Homomorphism of IL,CL; ::_thesis: for i, k, j being Element of IL st f is one-to-one & (f . i) "/\" (f . k) [= f . j holds
f . k [= f . (i => j)
let i, k, j be Element of IL; ::_thesis: ( f is one-to-one & (f . i) "/\" (f . k) [= f . j implies f . k [= f . (i => j) )
assume A1: f is one-to-one ; ::_thesis: ( not (f . i) "/\" (f . k) [= f . j or f . k [= f . (i => j) )
hereby ::_thesis: verum
assume (f . i) "/\" (f . k) [= f . j ; ::_thesis: f . k [= f . (i => j)
then f . (i "/\" k) [= f . j by Def1;
then i "/\" k [= j by A1, Th5;
then k [= i => j by FILTER_0:def_7;
hence f . k [= f . (i => j) by Th4; ::_thesis: verum
end;
end;
theorem :: LATTICE4:28
for CL being C_Lattice
for IL being implicative Lattice
for f being Homomorphism of IL,CL st f is bijective holds
( CL is implicative & f preserves_implication )
proof
let CL be C_Lattice; ::_thesis: for IL being implicative Lattice
for f being Homomorphism of IL,CL st f is bijective holds
( CL is implicative & f preserves_implication )
let IL be implicative Lattice; ::_thesis: for f being Homomorphism of IL,CL st f is bijective holds
( CL is implicative & f preserves_implication )
let f be Homomorphism of IL,CL; ::_thesis: ( f is bijective implies ( CL is implicative & f preserves_implication ) )
assume A1: f is bijective ; ::_thesis: ( CL is implicative & f preserves_implication )
thus CL is implicative ::_thesis: f preserves_implication
proof
let p, q be Element of CL; :: according to FILTER_0:def_6 ::_thesis: ex b1 being Element of the carrier of CL st
( p "/\" b1 [= q & ( for b2 being Element of the carrier of CL holds
( not p "/\" b2 [= q or b2 [= b1 ) ) )
consider i being Element of IL such that
A2: f . i = p by A1, Th6;
consider j being Element of IL such that
A3: f . j = q by A1, Th6;
take r = f . (i => j); ::_thesis: ( p "/\" r [= q & ( for b1 being Element of the carrier of CL holds
( not p "/\" b1 [= q or b1 [= r ) ) )
thus p "/\" r [= q by A2, A3, Th26; ::_thesis: for b1 being Element of the carrier of CL holds
( not p "/\" b1 [= q or b1 [= r )
hereby ::_thesis: verum
let r1 be Element of CL; ::_thesis: ( p "/\" r1 [= q implies r1 [= r )
assume A4: p "/\" r1 [= q ; ::_thesis: r1 [= r
ex k being Element of IL st f . k = r1 by A1, Th6;
hence r1 [= r by A1, A2, A3, A4, Th27; ::_thesis: verum
end;
end;
then reconsider CL = CL as implicative Lattice ;
reconsider f = f as Homomorphism of IL,CL ;
now__::_thesis:_for_i,_j_being_Element_of_IL_holds_(f_._i)_=>_(f_._j)_=_f_._(i_=>_j)
let i, j be Element of IL; ::_thesis: (f . i) => (f . j) = f . (i => j)
A5: now__::_thesis:_for_r1_being_Element_of_CL_st_(f_._i)_"/\"_r1_[=_f_._j_holds_
r1_[=_f_._(i_=>_j)
let r1 be Element of CL; ::_thesis: ( (f . i) "/\" r1 [= f . j implies r1 [= f . (i => j) )
assume A6: (f . i) "/\" r1 [= f . j ; ::_thesis: r1 [= f . (i => j)
ex k being Element of IL st f . k = r1 by A1, Th6;
hence r1 [= f . (i => j) by A1, A6, Th27; ::_thesis: verum
end;
(f . i) "/\" (f . (i => j)) [= f . j by Th26;
hence (f . i) => (f . j) = f . (i => j) by A5, FILTER_0:def_7; ::_thesis: verum
end;
hence f preserves_implication by Def3; ::_thesis: verum
end;
begin
theorem Th29: :: LATTICE4:29
for BL being Boolean Lattice holds (Top BL) ` = Bottom BL
proof
let BL be Boolean Lattice; ::_thesis: (Top BL) ` = Bottom BL
set a = Bottom BL;
thus (Top BL) ` = ((Bottom BL) "\/" ((Bottom BL) `)) ` by LATTICES:21
.= ((Bottom BL) `) "/\" (((Bottom BL) `) `)
.= Bottom BL ; ::_thesis: verum
end;
theorem Th30: :: LATTICE4:30
for BL being Boolean Lattice holds (Bottom BL) ` = Top BL
proof
let BL be Boolean Lattice; ::_thesis: (Bottom BL) ` = Top BL
set a = Top BL;
thus (Bottom BL) ` = ((Top BL) "/\" ((Top BL) `)) ` by LATTICES:20
.= ((Top BL) `) "\/" (((Top BL) `) `)
.= Top BL ; ::_thesis: verum
end;
theorem :: LATTICE4:31
for CL being C_Lattice
for BL being Boolean Lattice
for f being Homomorphism of BL,CL st f is onto holds
( CL is Boolean & f preserves_complement )
proof
let CL be C_Lattice; ::_thesis: for BL being Boolean Lattice
for f being Homomorphism of BL,CL st f is onto holds
( CL is Boolean & f preserves_complement )
let BL be Boolean Lattice; ::_thesis: for f being Homomorphism of BL,CL st f is onto holds
( CL is Boolean & f preserves_complement )
let f be Homomorphism of BL,CL; ::_thesis: ( f is onto implies ( CL is Boolean & f preserves_complement ) )
assume A1: f is onto ; ::_thesis: ( CL is Boolean & f preserves_complement )
then A2: f preserves_top by Th18;
thus ( CL is bounded & CL is complemented ) ; :: according to LATTICES:def_20 ::_thesis: ( CL is distributive & f preserves_complement )
thus CL is distributive by A1, Th11; ::_thesis: f preserves_complement
then reconsider CL = CL as Boolean Lattice ;
A3: f preserves_bottom by A1, Th12;
reconsider f = f as Homomorphism of BL,CL ;
now__::_thesis:_for_a1_being_Element_of_BL_holds_(f_._a1)_`_=_f_._(a1_`)
let a1 be Element of BL; ::_thesis: (f . a1) ` = f . (a1 `)
A4: (f . (a1 `)) "/\" (f . a1) = f . ((a1 `) "/\" a1) by Def1
.= f . (Bottom BL) by LATTICES:20
.= Bottom CL by A3, Def5 ;
(f . (a1 `)) "\/" (f . a1) = f . ((a1 `) "\/" a1) by Def1
.= f . (Top BL) by LATTICES:21
.= Top CL by A2, Def4 ;
then f . (a1 `) is_a_complement_of f . a1 by A4, LATTICES:def_18;
hence (f . a1) ` = f . (a1 `) by LATTICES:def_21; ::_thesis: verum
end;
hence f preserves_complement by Def6; ::_thesis: verum
end;
definition
let BL be Boolean Lattice;
mode Field of BL -> non empty Subset of BL means :Def9: :: LATTICE4:def 9
for a, b being Element of BL st a in it & b in it holds
( a "/\" b in it & a ` in it );
existence
ex b1 being non empty Subset of BL st
for a, b being Element of BL st a in b1 & b in b1 holds
( a "/\" b in b1 & a ` in b1 )
proof
the carrier of BL c= the carrier of BL ;
then reconsider F = the carrier of BL as non empty Subset of BL ;
take F ; ::_thesis: for a, b being Element of BL st a in F & b in F holds
( a "/\" b in F & a ` in F )
thus for a, b being Element of BL st a in F & b in F holds
( a "/\" b in F & a ` in F ) ; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines Field LATTICE4:def_9_:_
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 Th32: :: LATTICE4:32
for BL being Boolean Lattice
for a, b being Element of BL
for F being Field of BL st a in F & b in F holds
a "\/" b in F
proof
let BL be Boolean Lattice; ::_thesis: for a, b being Element of BL
for F being Field of BL st a in F & b in F holds
a "\/" b in F
let a, b be Element of BL; ::_thesis: for F being Field of BL st a in F & b in F holds
a "\/" b in F
let F be Field of BL; ::_thesis: ( a in F & b in F implies a "\/" b in F )
assume ( a in F & b in F ) ; ::_thesis: a "\/" b in F
then ( a ` in F & b ` in F ) by Def9;
then (a `) "/\" (b `) in F by Def9;
then (a "\/" b) ` in F by LATTICES:24;
then ((a "\/" b) `) ` in F by Def9;
hence a "\/" b in F by LATTICES:22; ::_thesis: verum
end;
theorem Th33: :: LATTICE4:33
for BL being Boolean Lattice
for a, b being Element of BL
for F being Field of BL st a in F & b in F holds
a => b in F
proof
let BL be Boolean Lattice; ::_thesis: for a, b being Element of BL
for F being Field of BL st a in F & b in F holds
a => b in F
let a, b be Element of BL; ::_thesis: for F being Field of BL st a in F & b in F holds
a => b in F
let F be Field of BL; ::_thesis: ( a in F & b in F implies a => b in F )
assume that
A1: a in F and
A2: b in F ; ::_thesis: a => b in F
a ` in F by A1, Def9;
then (a `) "\/" b in F by A2, Th32;
hence a => b in F by FILTER_0:42; ::_thesis: verum
end;
theorem Th34: :: LATTICE4:34
for BL being Boolean Lattice holds the carrier of BL is Field of BL
proof
let BL be Boolean Lattice; ::_thesis: the carrier of BL is Field of BL
the carrier of BL c= the carrier of BL ;
then reconsider F = the carrier of BL as non empty Subset of BL ;
for a, b being Element of BL st a in F & b in F holds
( a "/\" b in F & a ` in F ) ;
hence the carrier of BL is Field of BL by Def9; ::_thesis: verum
end;
theorem Th35: :: LATTICE4:35
for BL being Boolean Lattice
for F being Field of BL holds F is ClosedSubset of BL
proof
let BL be Boolean Lattice; ::_thesis: for F being Field of BL holds F is ClosedSubset of BL
let F be Field of BL; ::_thesis: F is ClosedSubset of BL
A1: for a, b being Element of BL st a in F & b in F holds
a "/\" b in F by Def9;
for a, b being Element of BL st a in F & b in F holds
a "\/" b in F by Th32;
hence F is ClosedSubset of BL by A1, LATTICES:def_24, LATTICES:def_25; ::_thesis: verum
end;
definition
let BL be Boolean Lattice;
let A be non empty Subset of BL;
func field_by A -> Field of BL means :Def10: :: LATTICE4:def 10
( A c= it & ( for F being Field of BL st A c= F holds
it c= F ) );
existence
ex b1 being Field of BL st
( A c= b1 & ( for F being Field of BL st A c= F holds
b1 c= F ) )
proof
set x = the Element of A;
defpred S1[ set ] means ( $1 is Field of BL & A c= $1 );
consider X being set such that
A1: for Z being set holds
( Z in X iff ( Z in bool the carrier of BL & S1[Z] ) ) from XBOOLE_0:sch_1();
reconsider x = the Element of A as Element of BL ;
A2: the carrier of BL is Field of BL by Th34;
then A3: X <> {} by A1;
now__::_thesis:_for_Z_being_set_st_Z_in_X_holds_
x_in_Z
let Z be set ; ::_thesis: ( Z in X implies x in Z )
assume Z in X ; ::_thesis: x in Z
then A c= Z by A1;
hence x in Z by TARSKI:def_3; ::_thesis: verum
end;
then reconsider F1 = meet X as non empty set by A3, SETFAM_1:def_1;
A4: the carrier of BL in X by A1, A2;
F1 c= the carrier of BL
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F1 or x in the carrier of BL )
thus ( not x in F1 or x in the carrier of BL ) by A4, SETFAM_1:def_1; ::_thesis: verum
end;
then reconsider F1 = F1 as non empty Subset of BL ;
F1 is Field of BL
proof
let a be Element of BL; :: according to LATTICE4:def_9 ::_thesis: for b being Element of BL st a in F1 & b in F1 holds
( a "/\" b in F1 & a ` in F1 )
let b be Element of BL; ::_thesis: ( a in F1 & b in F1 implies ( a "/\" b in F1 & a ` in F1 ) )
assume that
A5: a in F1 and
A6: b in F1 ; ::_thesis: ( a "/\" b in F1 & a ` in F1 )
A7: for Z being set st Z in X holds
a "/\" b in Z
proof
let Z be set ; ::_thesis: ( Z in X implies a "/\" b in Z )
assume A8: Z in X ; ::_thesis: a "/\" b in Z
then A9: b in Z by A6, SETFAM_1:def_1;
( Z is Field of BL & a in Z ) by A1, A5, A8, SETFAM_1:def_1;
hence a "/\" b in Z by A9, Def9; ::_thesis: verum
end;
for Z being set st Z in X holds
a ` in Z
proof
let Z be set ; ::_thesis: ( Z in X implies a ` in Z )
assume Z in X ; ::_thesis: a ` in Z
then ( Z is Field of BL & a in Z ) by A1, A5, SETFAM_1:def_1;
hence a ` in Z by Def9; ::_thesis: verum
end;
hence ( a "/\" b in F1 & a ` in F1 ) by A3, A7, SETFAM_1:def_1; ::_thesis: verum
end;
then reconsider F = F1 as Field of BL ;
take F ; ::_thesis: ( A c= F & ( for F being Field of BL st A c= F holds
F c= F ) )
for Z being set st Z in X holds
A c= Z by A1;
hence A c= F by A4, SETFAM_1:5; ::_thesis: for F being Field of BL st A c= F holds
F c= F
let H be Field of BL; ::_thesis: ( A c= H implies F c= H )
assume A c= H ; ::_thesis: F c= H
then H in X by A1;
hence F c= H by SETFAM_1:3; ::_thesis: verum
end;
uniqueness
for b1, b2 being Field of BL st A c= b1 & ( for F being Field of BL st A c= F holds
b1 c= F ) & A c= b2 & ( for F being Field of BL st A c= F holds
b2 c= F ) holds
b1 = b2
proof
let F1, F2 be Field of BL; ::_thesis: ( A c= F1 & ( for F being Field of BL st A c= F holds
F1 c= F ) & A c= F2 & ( for F being Field of BL st A c= F holds
F2 c= F ) implies F1 = F2 )
assume ( A c= F1 & ( for F being Field of BL st A c= F holds
F1 c= F ) & A c= F2 & ( for F being Field of BL st A c= F holds
F2 c= F ) ) ; ::_thesis: F1 = F2
hence ( F1 c= F2 & F2 c= F1 ) ; :: according to XBOOLE_0:def_10 ::_thesis: verum
end;
end;
:: deftheorem Def10 defines field_by LATTICE4:def_10_:_
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 ) ) );
definition
let BL be Boolean Lattice;
let A be non empty Subset of BL;
func SetImp A -> Subset of BL equals :: LATTICE4:def 11
{ (a => b) where a, b is Element of BL : ( a in A & b in A ) } ;
coherence
{ (a => b) where a, b is Element of BL : ( a in A & b in A ) } is Subset of BL
proof
set B = { (a => b) where a, b is Element of BL : ( a in A & b in A ) } ;
{ (a => b) where a, b is Element of BL : ( a in A & b in A ) } c= the carrier of BL
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (a => b) where a, b is Element of BL : ( a in A & b in A ) } or x in the carrier of BL )
assume x in { (a => b) where a, b is Element of BL : ( a in A & b in A ) } ; ::_thesis: x in the carrier of BL
then ex p, q being Element of BL st
( x = p => q & p in A & q in A ) ;
hence x in the carrier of BL ; ::_thesis: verum
end;
hence { (a => b) where a, b is Element of BL : ( a in A & b in A ) } is Subset of BL ; ::_thesis: verum
end;
end;
:: deftheorem defines SetImp LATTICE4:def_11_:_
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 ) } ;
registration
let BL be Boolean Lattice;
let A be non empty Subset of BL;
cluster SetImp A -> non empty ;
coherence
not SetImp A is empty
proof
set x = the Element of A;
set B = { (a => b) where a, b is Element of BL : ( a in A & b in A ) } ;
reconsider x = the Element of A as Element of BL ;
x => x in { (a => b) where a, b is Element of BL : ( a in A & b in A ) } ;
then reconsider B = { (a => b) where a, b is Element of BL : ( a in A & b in A ) } as non empty set ;
B = SetImp A ;
hence not SetImp A is empty ; ::_thesis: verum
end;
end;
theorem :: LATTICE4:36
for x being set
for BL being Boolean Lattice
for A being non empty Subset of BL holds
( x in SetImp A iff ex p, q being Element of BL st
( x = p => q & p in A & q in A ) ) ;
theorem Th37: :: LATTICE4:37
for BL being Boolean Lattice
for A being non empty Subset of BL
for c being Element of BL holds
( c in SetImp A iff ex p, q being Element of BL st
( c = (p `) "\/" q & p in A & q in A ) )
proof
let BL be Boolean Lattice; ::_thesis: for A being non empty Subset of BL
for c being Element of BL holds
( c in SetImp A iff ex p, q being Element of BL st
( c = (p `) "\/" q & p in A & q in A ) )
let A be non empty Subset of BL; ::_thesis: for c being Element of BL holds
( c in SetImp A iff ex p, q being Element of BL st
( c = (p `) "\/" q & p in A & q in A ) )
let c be Element of BL; ::_thesis: ( c in SetImp A iff ex p, q being Element of BL st
( c = (p `) "\/" q & p in A & q in A ) )
hereby ::_thesis: ( ex p, q being Element of BL st
( c = (p `) "\/" q & p in A & q in A ) implies c in SetImp A )
assume c in SetImp A ; ::_thesis: ex p, q being Element of BL st
( c = (p `) "\/" q & p in A & q in A )
then consider p, q being Element of BL such that
A1: ( c = p => q & p in A & q in A ) ;
take p = p; ::_thesis: ex q being Element of BL st
( c = (p `) "\/" q & p in A & q in A )
take q = q; ::_thesis: ( c = (p `) "\/" q & p in A & q in A )
thus ( c = (p `) "\/" q & p in A & q in A ) by A1, FILTER_0:42; ::_thesis: verum
end;
given p, q being Element of BL such that A2: c = (p `) "\/" q and
A3: ( p in A & q in A ) ; ::_thesis: c in SetImp A
c = p => q by A2, FILTER_0:42;
hence c in SetImp A by A3; ::_thesis: verum
end;
definition
let BL be Boolean Lattice;
deffunc H1( Element of BL) -> Element of the carrier of BL = $1 ` ;
func comp BL -> Function of the carrier of BL, the carrier of BL means :Def12: :: LATTICE4:def 12
for a being Element of BL holds it . a = a ` ;
existence
ex b1 being Function of the carrier of BL, the carrier of BL st
for a being Element of BL holds b1 . a = a `
proof
consider f being Function of the carrier of BL, the carrier of BL such that
A1: for a being Element of BL holds f . a = H1(a) from FUNCT_2:sch_4();
take f ; ::_thesis: for a being Element of BL holds f . a = a `
thus for a being Element of BL holds f . a = a ` by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of the carrier of BL, the carrier of BL st ( for a being Element of BL holds b1 . a = a ` ) & ( for a being Element of BL holds b2 . a = a ` ) holds
b1 = b2
proof
thus for f1, f2 being Function of the carrier of BL, the carrier of BL st ( for x being Element of BL holds f1 . x = H1(x) ) & ( for x being Element of BL holds f2 . x = H1(x) ) holds
f1 = f2 from BINOP_2:sch_1(); ::_thesis: verum
end;
end;
:: deftheorem Def12 defines comp LATTICE4:def_12_:_
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 Th38: :: LATTICE4:38
for BL being Boolean Lattice
for b being Element of BL
for B being Finite_Subset of the carrier of BL holds FinJoin ((B \/ {.b.}),(comp BL)) = (FinJoin (B,(comp BL))) "\/" (b `)
proof
let BL be Boolean Lattice; ::_thesis: for b being Element of BL
for B being Finite_Subset of the carrier of BL holds FinJoin ((B \/ {.b.}),(comp BL)) = (FinJoin (B,(comp BL))) "\/" (b `)
let b be Element of BL; ::_thesis: for B being Finite_Subset of the carrier of BL holds FinJoin ((B \/ {.b.}),(comp BL)) = (FinJoin (B,(comp BL))) "\/" (b `)
let B be Finite_Subset of the carrier of BL; ::_thesis: FinJoin ((B \/ {.b.}),(comp BL)) = (FinJoin (B,(comp BL))) "\/" (b `)
thus FinJoin ((B \/ {.b.}),(comp BL)) = (FinJoin (B,(comp BL))) "\/" ((comp BL) . b) by Th13
.= (FinJoin (B,(comp BL))) "\/" (b `) by Def12 ; ::_thesis: verum
end;
theorem :: LATTICE4:39
for BL being Boolean Lattice
for B being Finite_Subset of the carrier of BL holds (FinJoin B) ` = FinMeet (B,(comp BL))
proof
let BL be Boolean Lattice; ::_thesis: for B being Finite_Subset of the carrier of BL holds (FinJoin B) ` = FinMeet (B,(comp BL))
let B be Finite_Subset of the carrier of BL; ::_thesis: (FinJoin B) ` = FinMeet (B,(comp BL))
set M = the L_meet of BL;
set J = the L_join of BL;
A1: for a, b being Element of BL holds (comp BL) . ( the L_join of BL . (a,b)) = the L_meet of BL . (((comp BL) . a),((comp BL) . b))
proof
let a, b be Element of BL; ::_thesis: (comp BL) . ( the L_join of BL . (a,b)) = the L_meet of BL . (((comp BL) . a),((comp BL) . b))
thus (comp BL) . ( the L_join of BL . (a,b)) = (a "\/" b) ` by Def12
.= (a `) "/\" (b `) by LATTICES:24
.= the L_meet of BL . (((comp BL) . a),(b `)) by Def12
.= the L_meet of BL . (((comp BL) . a),((comp BL) . b)) by Def12 ; ::_thesis: verum
end;
A2: (comp BL) . (the_unity_wrt the L_join of BL) = (the_unity_wrt the L_join of BL) ` by Def12
.= (Bottom BL) ` by LATTICE2:52
.= Top BL by Th30
.= the_unity_wrt the L_meet of BL by LATTICE2:57 ;
thus (FinJoin B) ` = ( the L_join of BL $$ (B,(id BL))) ` by LATTICE2:def_3
.= (comp BL) . ( the L_join of BL $$ (B,(id BL))) by Def12
.= the L_meet of BL $$ (B,((comp BL) * (id BL))) by A2, A1, SETWISEO:36
.= the L_meet of BL $$ (B,(comp BL)) by FUNCT_2:17
.= FinMeet (B,(comp BL)) by LATTICE2:def_4 ; ::_thesis: verum
end;
theorem :: LATTICE4:40
for BL being Boolean Lattice
for b being Element of BL
for B being Finite_Subset of the carrier of BL holds FinMeet ((B \/ {.b.}),(comp BL)) = (FinMeet (B,(comp BL))) "/\" (b `)
proof
let BL be Boolean Lattice; ::_thesis: for b being Element of BL
for B being Finite_Subset of the carrier of BL holds FinMeet ((B \/ {.b.}),(comp BL)) = (FinMeet (B,(comp BL))) "/\" (b `)
let b be Element of BL; ::_thesis: for B being Finite_Subset of the carrier of BL holds FinMeet ((B \/ {.b.}),(comp BL)) = (FinMeet (B,(comp BL))) "/\" (b `)
let B be Finite_Subset of the carrier of BL; ::_thesis: FinMeet ((B \/ {.b.}),(comp BL)) = (FinMeet (B,(comp BL))) "/\" (b `)
thus FinMeet ((B \/ {.b.}),(comp BL)) = (FinMeet (B,(comp BL))) "/\" ((comp BL) . b) by Th20
.= (FinMeet (B,(comp BL))) "/\" (b `) by Def12 ; ::_thesis: verum
end;
theorem Th41: :: LATTICE4:41
for BL being Boolean Lattice
for B being Finite_Subset of the carrier of BL holds (FinMeet B) ` = FinJoin (B,(comp BL))
proof
let BL be Boolean Lattice; ::_thesis: for B being Finite_Subset of the carrier of BL holds (FinMeet B) ` = FinJoin (B,(comp BL))
let B be Finite_Subset of the carrier of BL; ::_thesis: (FinMeet B) ` = FinJoin (B,(comp BL))
set M = the L_meet of BL;
set J = the L_join of BL;
A1: for a, b being Element of BL holds (comp BL) . ( the L_meet of BL . (a,b)) = the L_join of BL . (((comp BL) . a),((comp BL) . b))
proof
let a, b be Element of BL; ::_thesis: (comp BL) . ( the L_meet of BL . (a,b)) = the L_join of BL . (((comp BL) . a),((comp BL) . b))
thus (comp BL) . ( the L_meet of BL . (a,b)) = (a "/\" b) ` by Def12
.= (a `) "\/" (b `) by LATTICES:23
.= the L_join of BL . (((comp BL) . a),(b `)) by Def12
.= the L_join of BL . (((comp BL) . a),((comp BL) . b)) by Def12 ; ::_thesis: verum
end;
A2: (comp BL) . (the_unity_wrt the L_meet of BL) = (the_unity_wrt the L_meet of BL) ` by Def12
.= (Top BL) ` by LATTICE2:57
.= Bottom BL by Th29
.= the_unity_wrt the L_join of BL by LATTICE2:52 ;
thus (FinMeet B) ` = ( the L_meet of BL $$ (B,(id BL))) ` by LATTICE2:def_4
.= (comp BL) . ( the L_meet of BL $$ (B,(id BL))) by Def12
.= the L_join of BL $$ (B,((comp BL) * (id BL))) by A2, A1, SETWISEO:36
.= the L_join of BL $$ (B,(comp BL)) by FUNCT_2:17
.= FinJoin (B,(comp BL)) by LATTICE2:def_3 ; ::_thesis: verum
end;
theorem Th42: :: LATTICE4:42
for BL being Boolean Lattice
for AF being non empty ClosedSubset of BL st Bottom BL in AF & Top BL in AF holds
for B being Finite_Subset of the carrier of BL st B c= SetImp AF holds
ex B0 being Finite_Subset of the carrier of BL st
( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 )
proof
let BL be Boolean Lattice; ::_thesis: for AF being non empty ClosedSubset of BL st Bottom BL in AF & Top BL in AF holds
for B being Finite_Subset of the carrier of BL st B c= SetImp AF holds
ex B0 being Finite_Subset of the carrier of BL st
( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 )
let AF be non empty ClosedSubset of BL; ::_thesis: ( Bottom BL in AF & Top BL in AF implies for B being Finite_Subset of the carrier of BL st B c= SetImp AF holds
ex B0 being Finite_Subset of the carrier of BL st
( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 ) )
assume that
A1: Bottom BL in AF and
A2: Top BL in AF ; ::_thesis: for B being Finite_Subset of the carrier of BL st B c= SetImp AF holds
ex B0 being Finite_Subset of the carrier of BL st
( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 )
set C = { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } ;
A3: { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } c= SetImp AF
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } or x in SetImp AF )
assume x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } ; ::_thesis: x in SetImp AF
then consider A1, A2 being Finite_Subset of the carrier of BL such that
A4: x = (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) and
A5: ( A1 c= AF & A2 c= AF ) ;
consider p, q being Element of BL such that
A6: ( p = FinMeet A2 & q = FinJoin A1 ) ;
A7: x = (p `) "\/" q by A4, A6, Th41;
( p in AF & q in AF ) by A1, A2, A5, A6, Th17, Th24;
hence x in SetImp AF by A7, Th37; ::_thesis: verum
end;
defpred S1[ Finite_Subset of the carrier of BL] means ( $1 c= SetImp AF implies ex B0 being Finite_Subset of the carrier of BL st
( B0 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin ($1,(comp BL)) = FinMeet B0 ) );
let B be Finite_Subset of the carrier of BL; ::_thesis: ( B c= SetImp AF implies ex B0 being Finite_Subset of the carrier of BL st
( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 ) )
assume A8: B c= SetImp AF ; ::_thesis: ex B0 being Finite_Subset of the carrier of BL st
( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 )
A9: for B9 being Finite_Subset of the carrier of BL
for b being Element of BL st S1[B9] holds
S1[B9 \/ {.b.}]
proof
set J = the L_join of BL;
let B9 be Finite_Subset of the carrier of BL; ::_thesis: for b being Element of BL st S1[B9] holds
S1[B9 \/ {.b.}]
let b be Element of BL; ::_thesis: ( S1[B9] implies S1[B9 \/ {.b.}] )
assume A10: ( B9 c= SetImp AF implies ex B1 being Finite_Subset of the carrier of BL st
( B1 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin (B9,(comp BL)) = FinMeet B1 ) ) ; ::_thesis: S1[B9 \/ {.b.}]
assume A11: B9 \/ {b} c= SetImp AF ; ::_thesis: ex B0 being Finite_Subset of the carrier of BL st
( B0 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin ((B9 \/ {.b.}),(comp BL)) = FinMeet B0 )
then consider B1 being Finite_Subset of the carrier of BL such that
A12: B1 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } and
A13: FinJoin (B9,(comp BL)) = FinMeet B1 by A10, ZFMISC_1:137;
b in SetImp AF by A11, ZFMISC_1:137;
then consider p, q being Element of BL such that
A14: b = (p `) "\/" q and
A15: p in AF and
A16: q in AF by Th37;
A17: for x being set
for b being Element of BL st x in ( the L_join of BL [:] ((id BL),b)) .: B1 holds
ex a being Element of BL st
( a in B1 & x = a "\/" b )
proof
let x be set ; ::_thesis: for b being Element of BL st x in ( the L_join of BL [:] ((id BL),b)) .: B1 holds
ex a being Element of BL st
( a in B1 & x = a "\/" b )
let b be Element of BL; ::_thesis: ( x in ( the L_join of BL [:] ((id BL),b)) .: B1 implies ex a being Element of BL st
( a in B1 & x = a "\/" b ) )
assume A18: x in ( the L_join of BL [:] ((id BL),b)) .: B1 ; ::_thesis: ex a being Element of BL st
( a in B1 & x = a "\/" b )
( the L_join of BL [:] ((id BL),b)) .: B1 c= the carrier of BL by FUNCT_2:36;
then reconsider x = x as Element of BL by A18;
consider a being Element of BL such that
A19: a in B1 and
A20: x = ( the L_join of BL [:] ((id BL),b)) . a by A18, FUNCT_2:65;
x = the L_join of BL . (((id BL) . a),b) by A20, FUNCOP_1:48
.= a "\/" b by FUNCT_1:18 ;
hence ex a being Element of BL st
( a in B1 & x = a "\/" b ) by A19; ::_thesis: verum
end;
A21: ( the L_join of BL [:] ((id BL),p)) .: B1 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ( the L_join of BL [:] ((id BL),p)) .: B1 or x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } )
assume x in ( the L_join of BL [:] ((id BL),p)) .: B1 ; ::_thesis: x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) }
then consider a being Element of BL such that
A22: a in B1 and
A23: x = a "\/" p by A17;
a in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } by A12, A22;
then consider A1, A2 being Finite_Subset of the carrier of BL such that
A24: a = (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) and
A25: ( A1 c= AF & A2 c= AF ) ;
ex A19, A29 being Finite_Subset of the carrier of BL st
( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF )
proof
take A19 = A1 \/ {.p.}; ::_thesis: ex A29 being Finite_Subset of the carrier of BL st
( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF )
take A29 = A2; ::_thesis: ( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF )
x = ((FinJoin A1) "\/" p) "\/" (FinJoin (A2,(comp BL))) by A23, A24, LATTICES:def_5
.= (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) by Th14 ;
hence ( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF ) by A15, A25, ZFMISC_1:137; ::_thesis: verum
end;
hence x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } ; ::_thesis: verum
end;
A26: ( the L_join of BL [:] ((id BL),(q `))) .: B1 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ( the L_join of BL [:] ((id BL),(q `))) .: B1 or x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } )
assume x in ( the L_join of BL [:] ((id BL),(q `))) .: B1 ; ::_thesis: x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) }
then consider a being Element of BL such that
A27: a in B1 and
A28: x = a "\/" (q `) by A17;
a in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } by A12, A27;
then consider A1, A2 being Finite_Subset of the carrier of BL such that
A29: a = (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) and
A30: ( A1 c= AF & A2 c= AF ) ;
ex A19, A29 being Finite_Subset of the carrier of BL st
( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF )
proof
take A19 = A1; ::_thesis: ex A29 being Finite_Subset of the carrier of BL st
( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF )
take A29 = A2 \/ {.q.}; ::_thesis: ( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF )
x = (FinJoin A1) "\/" ((FinJoin (A2,(comp BL))) "\/" (q `)) by A28, A29, LATTICES:def_5
.= (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) by Th38 ;
hence ( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF ) by A16, A30, ZFMISC_1:137; ::_thesis: verum
end;
hence x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } ; ::_thesis: verum
end;
take (( the L_join of BL [:] ((id BL),p)) .: B1) \/ (( the L_join of BL [:] ((id BL),(q `))) .: B1) ; ::_thesis: ( (( the L_join of BL [:] ((id BL),p)) .: B1) \/ (( the L_join of BL [:] ((id BL),(q `))) .: B1) c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin ((B9 \/ {.b.}),(comp BL)) = FinMeet ((( the L_join of BL [:] ((id BL),p)) .: B1) \/ (( the L_join of BL [:] ((id BL),(q `))) .: B1)) )
b ` = ((p `) `) "/\" (q `) by A14, LATTICES:24
.= p "/\" (q `) ;
then FinJoin ((B9 \/ {.b.}),(comp BL)) = (FinMeet B1) "\/" (p "/\" (q `)) by A13, Th38
.= ((FinMeet B1) "\/" p) "/\" ((FinMeet B1) "\/" (q `)) by LATTICES:11
.= (FinMeet (( the L_join of BL [:] ((id BL),p)) .: B1)) "/\" ((FinMeet B1) "\/" (q `)) by Th25
.= (FinMeet (( the L_join of BL [:] ((id BL),p)) .: B1)) "/\" (FinMeet (( the L_join of BL [:] ((id BL),(q `))) .: B1)) by Th25
.= FinMeet ((( the L_join of BL [:] ((id BL),p)) .: B1) \/ (( the L_join of BL [:] ((id BL),(q `))) .: B1)) by Th23 ;
hence ( (( the L_join of BL [:] ((id BL),p)) .: B1) \/ (( the L_join of BL [:] ((id BL),(q `))) .: B1) c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin ((B9 \/ {.b.}),(comp BL)) = FinMeet ((( the L_join of BL [:] ((id BL),p)) .: B1) \/ (( the L_join of BL [:] ((id BL),(q `))) .: B1)) ) by A21, A26, XBOOLE_1:8; ::_thesis: verum
end;
A31: S1[ {}. the carrier of BL]
proof
assume {}. the carrier of BL c= SetImp AF ; ::_thesis: ex B0 being Finite_Subset of the carrier of BL st
( B0 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin (({}. the carrier of BL),(comp BL)) = FinMeet B0 )
take B0 = {.(Bottom BL).}; ::_thesis: ( B0 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin (({}. the carrier of BL),(comp BL)) = FinMeet B0 )
A32: B0 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B0 or x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } )
assume x in B0 ; ::_thesis: x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) }
then A33: x = Bottom BL by TARSKI:def_1;
ex A1, A2 being Finite_Subset of the carrier of BL st
( x = (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) & A1 c= AF & A2 c= AF )
proof
take A1 = {.(Bottom BL).}; ::_thesis: ex A2 being Finite_Subset of the carrier of BL st
( x = (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) & A1 c= AF & A2 c= AF )
take A2 = {.(Top BL).}; ::_thesis: ( x = (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) & A1 c= AF & A2 c= AF )
thus x = (Bottom BL) "\/" (Bottom BL) by A33
.= (Bottom BL) "\/" ((Top BL) `) by Th29
.= (FinJoin A1) "\/" ((Top BL) `) by Th9
.= (FinJoin A1) "\/" ((FinMeet A2) `) by Th10
.= (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) by Th41 ; ::_thesis: ( A1 c= AF & A2 c= AF )
thus A1 c= AF by A1, ZFMISC_1:31; ::_thesis: A2 c= AF
thus A2 c= AF by A2, ZFMISC_1:31; ::_thesis: verum
end;
hence x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } ; ::_thesis: verum
end;
FinJoin (({}. the carrier of BL),(comp BL)) = Bottom BL by Lm1
.= FinMeet {.(Bottom BL).} by Th10 ;
hence ( B0 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin (({}. the carrier of BL),(comp BL)) = FinMeet B0 ) by A32; ::_thesis: verum
end;
for B being Finite_Subset of the carrier of BL holds S1[B] from SETWISEO:sch_4(A31, A9);
then ex B1 being Finite_Subset of the carrier of BL st
( B1 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Finite_Subset of the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin (B,(comp BL)) = FinMeet B1 ) by A8;
hence ex B0 being Finite_Subset of the carrier of BL st
( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 ) by A3, XBOOLE_1:1; ::_thesis: verum
end;
theorem :: LATTICE4:43
for BL being Boolean Lattice
for AF being non empty ClosedSubset of BL st Bottom BL in AF & Top BL in AF holds
{ (FinMeet B) where B is Finite_Subset of the carrier of BL : B c= SetImp AF } = field_by AF
proof
let BL be Boolean Lattice; ::_thesis: for AF being non empty ClosedSubset of BL st Bottom BL in AF & Top BL in AF holds
{ (FinMeet B) where B is Finite_Subset of the carrier of BL : B c= SetImp AF } = field_by AF
let AF be non empty ClosedSubset of BL; ::_thesis: ( Bottom BL in AF & Top BL in AF implies { (FinMeet B) where B is Finite_Subset of the carrier of BL : B c= SetImp AF } = field_by AF )
assume that
A1: Bottom BL in AF and
A2: Top BL in AF ; ::_thesis: { (FinMeet B) where B is Finite_Subset of the carrier of BL : B c= SetImp AF } = field_by AF
set A1 = { (FinMeet B) where B is Finite_Subset of the carrier of BL : B c= SetImp AF } ;
A3: AF c= { (FinMeet B) where B is Finite_Subset of the carrier of BL : B c= SetImp AF }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in AF or x in { (FinMeet B) where B is Finite_Subset of the carrier of BL : B c= SetImp AF } )
assume A4: x in AF ; ::_thesis: x in { (FinMeet B) where B is Finite_Subset of the carrier of BL : B c= SetImp AF }
then reconsider b = x as Element of BL ;
reconsider B = {.b.} as Finite_Subset of the carrier of BL ;
b = (Bottom BL) "\/" b
.= ((Top BL) `) "\/" b by Th29 ;
then b in SetImp AF by A2, A4, Th37;
then A5: B c= SetImp AF by ZFMISC_1:31;
x = FinMeet B by Th10;
hence x in { (FinMeet B) where B is Finite_Subset of the carrier of BL : B c= SetImp AF } by A5; ::_thesis: verum
end;
{ (FinMeet B) where B is Finite_Subset of the carrier of BL : B c= SetImp AF } c= the carrier of BL
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (FinMeet B) where B is Finite_Subset of the carrier of BL : B c= SetImp AF } or x in the carrier of BL )
assume x in { (FinMeet B) where B is Finite_Subset of the carrier of BL : B c= SetImp AF } ; ::_thesis: x in the carrier of BL
then ex B being Finite_Subset of the carrier of BL st
( x = FinMeet B & B c= SetImp AF ) ;
hence x in the carrier of BL ; ::_thesis: verum
end;
then reconsider A1 = { (FinMeet B) where B is Finite_Subset of the carrier of BL : B c= SetImp AF } as non empty Subset of BL by A3;
A6: now__::_thesis:_for_F_being_Field_of_BL_st_AF_c=_F_holds_
A1_c=_F
let F be Field of BL; ::_thesis: ( AF c= F implies A1 c= F )
assume A7: AF c= F ; ::_thesis: A1 c= F
thus A1 c= F ::_thesis: verum
proof
reconsider F1 = F as ClosedSubset of BL by Th35;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A1 or x in F )
assume x in A1 ; ::_thesis: x in F
then consider B being Finite_Subset of the carrier of BL such that
A8: x = FinMeet B and
A9: B c= SetImp AF ;
SetImp AF c= F
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in SetImp AF or y in F )
assume y in SetImp AF ; ::_thesis: y in F
then ex p, q being Element of BL st
( y = p => q & p in AF & q in AF ) ;
hence y in F by A7, Th33; ::_thesis: verum
end;
then B c= F1 by A9, XBOOLE_1:1;
hence x in F by A2, A7, A8, Th24; ::_thesis: verum
end;
end;
A1 is Field of BL
proof
let p be Element of BL; :: according to LATTICE4:def_9 ::_thesis: for b being Element of BL st p in A1 & b in A1 holds
( p "/\" b in A1 & p ` in A1 )
let q be Element of BL; ::_thesis: ( p in A1 & q in A1 implies ( p "/\" q in A1 & p ` in A1 ) )
assume that
A10: p in A1 and
A11: q in A1 ; ::_thesis: ( p "/\" q in A1 & p ` in A1 )
thus p "/\" q in A1 ::_thesis: p ` in A1
proof
consider B2 being Finite_Subset of the carrier of BL such that
A12: ( q = FinMeet B2 & B2 c= SetImp AF ) by A11;
consider B1 being Finite_Subset of the carrier of BL such that
A13: ( p = FinMeet B1 & B1 c= SetImp AF ) by A10;
consider B0 being Finite_Subset of the carrier of BL such that
A14: B0 = B1 \/ B2 ;
( B0 c= SetImp AF & p "/\" q = FinMeet B0 ) by A13, A12, A14, Th23, XBOOLE_1:8;
hence p "/\" q in A1 ; ::_thesis: verum
end;
thus p ` in A1 ::_thesis: verum
proof
consider B being Finite_Subset of the carrier of BL such that
A15: p = FinMeet B and
A16: B c= SetImp AF by A10;
p ` = FinJoin (B,(comp BL)) by A15, Th41;
then ex B0 being Finite_Subset of the carrier of BL st
( B0 c= SetImp AF & p ` = FinMeet B0 ) by A1, A2, A16, Th42;
hence p ` in A1 ; ::_thesis: verum
end;
end;
hence { (FinMeet B) where B is Finite_Subset of the carrier of BL : B c= SetImp AF } = field_by AF by A3, A6, Def10; ::_thesis: verum
end;