Copyright (c) 1993 Association of Mizar Users
environ
vocabulary TARSKI, SETFAM_1, BOOLE, LATTICES, FILTER_0, GROUP_6, FUNCT_1,
MOD_4, RELAT_1, WELLORD1, FILTER_1, ZF_LANG, SUBSET_1, FINSUB_1,
LATTICE2, SETWISEO, BINOP_1, FUNCOP_1, VECTSP_1, LATTICE4, HAHNBAN;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, ORDINAL1,
FUNCT_1, FUNCT_2, BINOP_1, FINSUB_1, STRUCT_0, LATTICES, LATTICE2,
FILTER_0, FUNCOP_1, SETWISEO, GRCAT_1, WELLORD1, FILTER_1;
constructors BINOP_1, LATTICE2, SETWISEO, GRCAT_1, WELLORD1, FILTER_1,
DOMAIN_1, XBOOLE_0, TOPS_2;
clusters LATTICES, FILTER_0, STRUCT_0, FINSUB_1, RELSET_1, SUBSET_1, XBOOLE_0,
ZFMISC_1;
requirements BOOLE, SUBSET;
definitions TARSKI, FILTER_0, LATTICES, XBOOLE_0;
theorems LATTICES, ZFMISC_1, FUNCT_2, FILTER_0, SETFAM_1, ORDERS_2, TARSKI,
TMAP_1, SETWISEO, LATTICE2, FUNCOP_1, FILTER_1, WELLORD1, RELAT_1,
XBOOLE_0, XBOOLE_1;
schemes FUNCT_2, SETWISEO, COMPLSP1, XBOOLE_0;
begin :: Preliminaries
reserve x,y,X,X1,Y,Z for set;
theorem
union Y c= Z & X in Y implies X c= Z
proof
assume that
A1: union Y c= Z and
A2: X in Y;
thus X c= Z
proof let x be set;
assume x in X;
then x in union Y by A2,TARSKI:def 4;
hence x in Z by A1;
end;
end;
theorem
union INTERSECTION(X,Y) = union X /\ union Y
proof
thus union INTERSECTION(X,Y) c= union X /\ union Y by SETFAM_1:39;
let x be set;
assume x in union X /\ union Y;
then A1: x in union X & x in union Y by XBOOLE_0:def 3;
then consider X0 being set such that
A2: x in X0 & X0 in X by TARSKI:def 4;
consider Y0 being set such that
A3: x in Y0 & Y0 in Y by A1,TARSKI:def 4;
A4: X0 /\ Y0 in INTERSECTION(X,Y) by A2,A3,SETFAM_1:def 5;
x in X0 /\ Y0 by A2,A3,XBOOLE_0:def 3;
hence x in union INTERSECTION(X,Y) by A4,TARSKI:def 4;
end;
theorem
for X st X <> {} &
for Z st Z <> {} & Z c= X &
Z is c=-linear
ex Y st Y in X & for X1 st X1 in Z holds X1 c= Y
ex Y st Y in X & for Z st Z in X & Z <> Y holds not Y c= Z
proof
let X such that
A1: X <> {} &
for Z st Z <> {} & Z c= X & Z is c=-linear
ex Y st Y in X & for X1 st X1 in Z holds X1 c= Y;
for Z st Z c= X & Z is c=-linear
ex Y st Y in X & for X1 st X1 in Z holds X1 c= Y
proof
let Z such that
A2: Z c= X & Z is c=-linear;
per cases;
suppose A3: Z = {};
consider Y being Element of X;
for X1 st X1 in Z holds X1 c= Y by A3;
hence ex Y st Y in X & for X1 st X1 in Z holds X1 c= Y by A1;
suppose Z <> {};
hence ex Y st Y in X & for X1 st X1 in Z holds X1 c= Y by A1,A2;
end;
hence thesis by A1,ORDERS_2:77;
end;
begin :: Lattice Theory
reserve L for Lattice;
reserve F,H for Filter of L;
reserve p,q,r for Element of L;
theorem
<.L.) is prime
proof
let p,q;
p in the carrier of L & q in the carrier of L & p"\/"q in the carrier of L
;
hence p"\/"q in<.L.) iff p in <.L.) or q in <.L.) by FILTER_0:def 2;
end;
theorem
F c= <.F \/ H.) & H c= <.F \/ H.)
proof
A1: F c= F \/ H & H c= F \/ H by XBOOLE_1:7;
F \/ H c= <.F \/ H.) by FILTER_0:def 5;
hence thesis by A1,XBOOLE_1:1;
end;
theorem
p in <.<.q.) \/ F.) implies ex r st r in F & q "/\" r [= p
proof
assume A1: p in <.<.q.) \/ F.);
<.<.q.) \/ F.)={r : ex p',q' being Element of L st
p'"/\"q' [= r & p' in <.q.) & q' in F} by FILTER_0:48;
then ex r st r=p & ex p',q' being Element of L st
p'"/\"q' [= r & p' in <.q.) & q' in F by A1;
then consider p',q' being Element of L such that
A2: p' "/\" q' [= p & p' in <.q.) & q' in F;
q [= p' by A2,FILTER_0:18;
then q "/\" q' [= p' "/\" q' by LATTICES:27;
then q "/\" q' [= p by A2,LATTICES:25;
hence thesis by A2;
end;
reserve L1, L2 for Lattice;
reserve a1,b1 for Element of L1;
reserve a2 for Element of L2;
definition let L1,L2;
mode Homomorphism of L1,L2 ->
Function of the carrier of L1, the carrier of L2 means
:Def1: it.(a1 "\/" b1) = it.a1 "\/" it.b1 &
it.(a1 "/\" b1) = it.a1 "/\" it.b1;
existence
proof
consider b being Element of L2;
defpred P[set,set] means for a1 st $1=a1 holds $2=b;
A1: now let x be Element of L1;
take b;
thus P[x,b];
end;
consider f being Function of the carrier of L1,the carrier of L2 such that
A2: for x being Element of L1 holds P[x,f.x]
from FuncExD(A1);
take f;
now
let a1,b1;
thus f.(a1 "\/" b1) = b by A2
.= b "\/" b by LATTICES:17
.= f.a1 "\/" b by A2
.= f.a1 "\/" f.b1 by A2;
thus f.(a1 "/\" b1) = b by A2
.= b "/\" b by LATTICES:18
.= f.a1 "/\" b by A2
.= f.a1 "/\" f.b1 by A2;
end;
hence thesis;
end;
end;
reserve f for Homomorphism of L1,L2;
theorem Th7:
a1 [= b1 implies f.a1 [= f.b1
proof
assume A1:a1 [= b1;
thus f.a1 [= f.b1
proof
thus f.a1 "\/" f.b1 = f.(a1 "\/" b1) by Def1
.=f.b1 by A1,LATTICES:def 3;
end;
end;
definition let L1,L2;
let f be Function of the carrier of L1, the carrier of L2;
attr f is monomorphism means
:Def2: f is one-to-one;
attr f is epimorphism means
:Def3: rng f = the carrier of L2;
end;
theorem
Th8: f is monomorphism implies (a1 [= b1 iff (f.a1) [= (f.b1))
proof
assume f is monomorphism;
then A1: f is one-to-one by Def2;
reconsider 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;
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:25;
end;
hence thesis by Th7;
end;
theorem Th9:
for f being Function of the carrier of L1, the carrier of L2 holds
f is epimorphism implies (for a2 ex a1 st a2 = f.a1)
proof
let f be Function of the carrier of L1, the carrier of L2;
assume A1: f is epimorphism;
reconsider g = f as Function of the carrier of L1,the carrier of L2;
A2:rng g = the carrier of L2 by A1,Def3;
now let a2 be Element of L2;
consider x be set such that
A3: x in the carrier of L1 & g.x = a2 by A2,FUNCT_2:17;
thus ex a1 st g.a1 = a2 by A3;
end;
hence thesis;
end;
definition
let L1,L2,f;
attr f is isomorphism means
:Def4: f is monomorphism epimorphism;
end;
definition let L1,L2;
redefine pred L1,L2 are_isomorphic means
ex f st f is isomorphism;
compatibility
proof
thus L1,L2 are_isomorphic implies ex f st f is isomorphism
proof
assume L1,L2 are_isomorphic;
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;
set R = LattRel L1, S = LattRel L2;
A2: field S = the carrier of L2 & field R = the carrier of L1 by FILTER_1:33;
A3: dom F = field R & rng F = field S & F is one-to-one &
for a,b being set holds [a,b] in R iff
a in field R & b in field R & [F.a,F.b] in S by A1,WELLORD1:def 7;
then reconsider F as Function of the carrier of L1,
the carrier of L2 by A2,FUNCT_2:3;
now let a1,b1 be Element of L1;
reconsider a1'=a1,b1'=b1 as Element of L1;
A4: F is epimorphism by A2,A3,Def3;
thus F.(a1 "\/" b1) = F.a1 "\/" F.b1
proof
consider k1 being Element of L1 such that
A5: F.a1 "\/" F.b1 = F.k1 by A4,Th9;
F.a1 [= F.k1 & F.b1 [= F.k1 by A5,LATTICES:22;
then [F.a1,F.k1] in LattRel L2 & [F.b1,F.k1] in LattRel L2 by FILTER_1
:32;
then [a1,k1] in LattRel L1 & [b1,k1] in LattRel L1 by A1,A2,WELLORD1:
def 7;
then a1 [= k1 & b1 [= k1 by FILTER_1:32;
then a1 "\/" b1 [= k1 by FILTER_0:6;
then [a1 "\/" b1,k1] in R by FILTER_1:32;
then [F.(a1 "\/" b1),F.k1] in LattRel L2 by A1,WELLORD1:def 7;
then A6: F.(a1 "\/" b1) [= F.a1 "\/" F.b1 by A5,FILTER_1:32;
a1' [= a1' "\/" b1' by LATTICES:22;
then [a1,a1 "\/" b1] in R by FILTER_1:32;
then [F.a1,F.(a1 "\/" b1)] in S by A1,WELLORD1:def 7;
then A7: F.a1' [= F.(a1' "\/" b1') by FILTER_1:32;
b1' [= a1' "\/" b1' by LATTICES:22;
then [b1,a1 "\/" b1] in R by FILTER_1:32;
then [F.b1,F.(a1 "\/" b1)] in S by A1,WELLORD1:def 7;
then F.b1' [= F.(a1' "\/" b1') by FILTER_1:32;
then F.a1 "\/" F.b1 [= F.(a1 "\/" b1) by A7,FILTER_0:6;
hence thesis by A6,LATTICES:26;
end;
thus F.(a1 "/\" b1) = F.a1 "/\" F.b1
proof
consider k1 being Element of L1 such that
A8: F.a1 "/\" F.b1 = F.k1 by A4,Th9;
F.k1 [= F.a1 & F.k1 [= F.b1 by A8,LATTICES:23;
then [F.k1,F.a1] in LattRel L2 & [F.k1,F.b1] in LattRel L2 by FILTER_1
:32;
then [k1,a1] in LattRel L1 & [k1,b1] in LattRel L1 by A1,A2,WELLORD1:
def 7;
then k1 [= a1 & k1 [= b1 by FILTER_1:32;
then k1 [= a1 "/\" b1 by FILTER_0:7;
then [k1,a1 "/\" b1] in LattRel L1 by FILTER_1:32;
then [F.k1,F.(a1 "/\" b1)] in LattRel L2 by A1,WELLORD1:def 7;
then A9: F.a1 "/\" F.b1 [= F.(a1 "/\" b1) by A8,FILTER_1:32;
a1' "/\" b1' [= a1' by LATTICES:23;
then [a1 "/\" b1,a1] in R by FILTER_1:32;
then [F.(a1 "/\" b1),F.a1] in S by A1,WELLORD1:def 7;
then A10: F.(a1' "/\" b1') [= F.a1' by FILTER_1:32;
a1' "/\" b1' [= b1' by LATTICES:23;
then [a1 "/\" b1,b1] in R by FILTER_1:32;
then [F.(a1 "/\" b1),F.b1] in S by A1,WELLORD1:def 7;
then F.(a1' "/\" b1') [= F.b1' by FILTER_1:32;
then F.(a1 "/\" b1) [= F.a1 "/\" F.b1 by A10,FILTER_0:7;
hence thesis by A9,LATTICES:26;
end;
end;
then reconsider F as Homomorphism of L1,L2 by Def1;
take F;
F is monomorphism epimorphism by A2,A3,Def2,Def3;
hence thesis by Def4;
end;
given f such that
A11:f is isomorphism;
A12: f is monomorphism epimorphism by A11,Def4;
then A13:f is one-to-one by Def2;
set R = LattRel L1, S = LattRel L2;
A14:dom f = the carrier of L1 by FUNCT_2:def 1
.= field R by FILTER_1:33;
A15:rng f = the carrier of L2 by A12,Def3
.= field S by FILTER_1:33;
for a,b be set holds [a,b] in R iff
a in field R & b in field R & [f.a,f.b] in S
proof
let a,b be set;
hereby assume A16: [a,b] in R;
hence a in field R & b in field R by RELAT_1:30;
then reconsider a'=a,b'=b as Element of L1 by FILTER_1:33
;
a' [= b' by A16,FILTER_1:32;
then f.a' [= f.b' by A12,Th8;
hence [f.a,f.b] in S by FILTER_1:32;
end;
assume A17:a in field R & b in field R & [f.a,f.b] in S;
then reconsider a'=a,b'=b as Element of L1 by FILTER_1:33;
f.a' [= f.b' by A17,FILTER_1:32;
then a' [= b' by A12,Th8;
hence thesis by FILTER_1:32;
end;
then f is_isomorphism_of LattRel L1, LattRel L2 by A13,A14,A15,WELLORD1:def
7;
then LattRel L1, LattRel L2 are_isomorphic by WELLORD1:def 8;
hence thesis by FILTER_1:def 9;
end;
end;
definition
let L1,L2,f;
pred f preserves_implication means
:Def6: f.(a1 => b1) = (f.a1) => (f.b1);
pred f preserves_top means
:Def7: f.(Top L1) = Top L2;
pred f preserves_bottom means
:Def8: f.(Bottom L1) = Bottom L2;
pred f preserves_complement means
:Def9: f.(a1`) = (f.a1)`;
end;
definition let L;
mode ClosedSubset of L -> Subset of L means
:Def10: p in it & q in it implies p "/\" q in it & p "\/" q in it;
existence
proof
the carrier of L c= the carrier of L;
then reconsider F = the carrier of L as non empty Subset of L
;
take F;
thus thesis;
end;
end;
theorem Th10:
the carrier of L is ClosedSubset of L
proof
the carrier of L c= the carrier of L;
then reconsider F=the carrier of L as Subset of L;
p in F & q in F implies p "/\" q in F & p "\/" q in F;
hence the carrier of L is ClosedSubset of L by Def10;
end;
definition let L;
cluster non empty ClosedSubset of L;
existence
proof
the carrier of L is ClosedSubset of L by Th10;
hence thesis;
end;
end;
theorem
for F being Filter of L holds F is ClosedSubset of L
proof
let F be Filter of L;
for p,q st p in F & q in F holds
p "/\" q in F & p "\/" q in F by FILTER_0:10,def 1;
hence F is ClosedSubset of L by Def10;
end;
reserve B for Finite_Subset of the carrier of L;
definition let L,B;
canceled;
func FinJoin B -> Element of L equals
:Def12: FinJoin (B,id L);
correctness;
func FinMeet B -> Element of L equals
:Def13: FinMeet (B,id L);
correctness;
end;
canceled 2;
theorem Th14:
FinMeet B = (the L_meet of L) $$ (B,id L)
proof
thus FinMeet B = FinMeet(B,id L) by Def13
.= (the L_meet of L) $$ (B,id L) by LATTICE2:def 4;
end;
theorem Th15:
FinJoin B = (the L_join of L) $$ (B,id L)
proof
thus FinJoin B = FinJoin(B,id L) by Def12
.= (the L_join of L) $$ (B,id L) by LATTICE2:def 3;
end;
theorem Th16:
FinJoin {p} = p
proof set J=the L_join of L;
A1: J is commutative associative by LATTICE2:27,29;
thus FinJoin {p} =(the L_join of L) $$ ({p},id L) by Th15
.= (id L).p by A1,SETWISEO:26
.= p by TMAP_1:91;
end;
theorem Th17:
FinMeet {p} = p
proof
set M = the L_meet of L;
A1: M is commutative associative by LATTICE2:31,32;
thus FinMeet {p} = M $$ ({p},id L) by Th14
.= (id L).p by A1,SETWISEO:26
.= p by TMAP_1:91;
end;
begin :: Distributive Lattices
reserve DL for distributive Lattice;
reserve f for Homomorphism of DL,L2;
theorem Th18:
f is epimorphism implies L2 is distributive
proof
assume A1:f is epimorphism;
thus L2 is distributive
proof
let a,b,c be Element of L2;
consider a' be Element of DL such that
A2: f.a'=a by A1,Th9;
consider b' be Element of DL such that
A3: f.b'=b by A1,Th9;
consider c' be Element of DL such that
A4: f.c'=c by A1,Th9;
thus a"/\"(b"\/"c) = a"/\"f.(b'"\/"c') by A3,A4,Def1
.= f.(a'"/\"(b'"\/"c')) by A2,Def1
.=f.((a'"/\"b')"\/"(a'"/\"c')) by LATTICES:def 11
.=f.(a'"/\"b')"\/"f.(a'"/\"c') by Def1
.=(a"/\"b)"\/"f.(a'"/\"c') by A2,A3,Def1
.=(a"/\"b)"\/"(a"/\"c) by A2,A4,Def1;
end;
end;
begin :: Lower-bounded Lattices
reserve 0L for lower-bounded Lattice,
B,B1,B2 for Finite_Subset of the carrier of 0L,
b for Element of 0L;
theorem Th19:
for f being Homomorphism of 0L,L2 st f is epimorphism
holds L2 is lower-bounded & f preserves_bottom
proof let f be Homomorphism of 0L,L2;
assume A1: f is epimorphism;
set r = f.(Bottom 0L);
A2: now let a2 be Element of L2;
consider a1 be Element of 0L such that
A3: f.a1 = a2 by A1,Th9;
thus r"/\"a2 = f.(Bottom 0L "/\" a1) by A3,Def1
.= r by LATTICES:40;
hence a2"/\"r = r;
end;
thus L2 is lower-bounded
proof
take r;
thus thesis by A2;
end;
then Bottom L2=r by A2,LATTICES:def 16;
hence thesis by Def8;
end;
reserve f for UnOp of the carrier of 0L;
theorem Th20:
FinJoin(B \/ {b},f) = FinJoin (B,f) "\/" f.b
proof
set J= the L_join of 0L;
A1: J is idempotent & J is commutative & J is associative
& J has_a_unity by LATTICE2:26,27,29,67;
thus FinJoin (B \/ {b},f) = J $$ (B \/ {b},f) by LATTICE2:def 3
.= J.(J $$ (B,f),f.b) by A1,SETWISEO:41
.= J $$ (B,f) "\/" f.b by LATTICES:def 1
.= FinJoin (B,f) "\/" f.b by LATTICE2:def 3;
end;
theorem Th21:
FinJoin(B \/ {b}) = FinJoin B "\/" b
proof
thus FinJoin(B \/ {b}) = FinJoin(B \/ {b},id 0L) by Def12
.=FinJoin (B,id 0L) "\/" (id 0L).b by Th20
.=FinJoin (B,id 0L) "\/" b by TMAP_1:91
.= FinJoin B "\/" b by Def12;
end;
theorem
FinJoin B1 "\/" FinJoin B2 = FinJoin (B1 \/ B2)
proof
set J= the L_join of 0L;
A1: J is idempotent & J is commutative & J is associative
& J has_a_unity by LATTICE2:26,27,29,67;
thus FinJoin (B1 \/ B2) = J $$ (B1 \/ B2,id 0L) by Th15
.= J.(J $$ (B1,id 0L ),J $$ (B2,id 0L)) by A1,SETWISEO:42
.= J $$ (B1,id 0L) "\/" J $$ (B2,id 0L) by LATTICES:def 1
.= FinJoin B1 "\/" J $$ (B2,id 0L) by Th15
.=FinJoin B1 "\/" FinJoin B2 by Th15;
end;
Lm1:
for f being Function of the carrier of 0L , the carrier of 0L
holds FinJoin ({}.the carrier of 0L,f) = Bottom 0L
proof let f be Function of the carrier of 0L , the carrier of 0L;
set J=the L_join of 0L;
A1: J is commutative & J is associative & J has_a_unity
by LATTICE2:27,29,67;
thus FinJoin ({}.the carrier of 0L,f)
= J $$ ({}.the carrier of 0L,f) by LATTICE2:def 3
.= the_unity_wrt J by A1,SETWISEO:40
.= Bottom 0L by LATTICE2:68;
end;
theorem Th23:
FinJoin {}.the carrier of 0L = Bottom 0L
proof
thus FinJoin {}.the carrier of 0L
= FinJoin ({}.the carrier of 0L,id 0L) by Def12
.= Bottom 0L by Lm1;
end;
theorem
Th24: for A being ClosedSubset of 0L st Bottom 0L in A
for B holds B c= A implies FinJoin B in A
proof
let A be ClosedSubset of 0L;
defpred X[Finite_Subset of the carrier of 0L] means
$1 c= A implies FinJoin $1 in A;
assume Bottom 0L in A;
then
A1: X[{}.the carrier of 0L] by Th23;
A2: for B1 being Finite_Subset of the carrier of 0L
for p being Element of 0L st X[B1]
holds X[B1 \/ {p}]
proof
let B1 be Finite_Subset of the carrier of 0L;
let p be Element of 0L;
assume A3: B1 c=A implies FinJoin B1 in A;
assume A4: B1 \/ {p} c=A;
then {p} c= A by XBOOLE_1:11;
then p in A by ZFMISC_1:37;
then FinJoin B1 "\/" p in A by A3,A4,Def10,XBOOLE_1:11;
hence thesis by Th21;
end;
thus for B being Element of Fin the carrier of 0L
holds X[B] from FinSubInd3(A1,A2);
end;
begin :: Upper-bounded Lattices
reserve 1L for upper-bounded Lattice,
B,B1,B2 for Finite_Subset of the carrier of 1L,
b for Element of 1L;
theorem Th25:
for f being Homomorphism of 1L,L2 st f is epimorphism
holds L2 is upper-bounded & f preserves_top
proof let f be Homomorphism of 1L,L2;
assume A1: f is epimorphism;
set r = f.(Top 1L);
A2: now let a2 be Element of L2;
consider a1 be Element of 1L such that
A3: f.a1 = a2 by A1,Th9;
thus r"\/"a2 = f.(Top 1L "\/" a1) by A3,Def1
.= r by LATTICES:44;
hence a2"\/"r = r;
end;
thus L2 is upper-bounded
proof
take r;
thus thesis by A2;
end;
then Top L2=r by A2,LATTICES:def 17;
hence thesis by Def7;
end;
Lm2:
for f being Function of the carrier of 1L, the carrier of 1L
holds FinMeet ({}.the carrier of 1L,f) = Top 1L
proof
let f be Function of the carrier of 1L, the carrier of 1L;
set M=the L_meet of 1L;
A1: M is commutative associative & M has_a_unity
by LATTICE2:31,32,73;
thus FinMeet ({}.the carrier of 1L,f)
= M $$ ({}.the carrier of 1L,f) by LATTICE2:def 4
.= the_unity_wrt M by A1,SETWISEO:40
.= Top 1L by LATTICE2:74;
end;
theorem Th26:
FinMeet {}.the carrier of 1L = Top 1L
proof
thus FinMeet {}.the carrier of 1L
= FinMeet ({}.the carrier of 1L,id 1L) by Def13
.= Top 1L by Lm2;
end;
reserve f,g for UnOp of the carrier of 1L;
theorem Th27:
FinMeet(B \/ {b},f) = FinMeet (B,f) "/\" f.b
proof
set M= the L_meet of 1L;
A1: M is idempotent & M is commutative & M is associative
& M has_a_unity by LATTICE2:30,31,32,73;
thus FinMeet (B \/ {b},f) = M $$ (B \/ {b},f) by LATTICE2:def 4
.= M.(M $$ (B,f),f.b) by A1,SETWISEO:41
.= M $$ (B,f) "/\" f.b by LATTICES:def 2
.= FinMeet (B,f) "/\" f.b by LATTICE2:def 4;
end;
theorem Th28:
FinMeet(B \/ {b}) = FinMeet B "/\" b
proof
thus FinMeet(B \/ {b}) = FinMeet(B \/ {b},id 1L) by Def13
.=FinMeet (B,id 1L) "/\" (id 1L).b by Th27
.=FinMeet (B,id 1L) "/\" b by TMAP_1:91
.= FinMeet B "/\" b by Def13;
end;
theorem Th29:
FinMeet(f.:B,g) = FinMeet(B,g*f)
proof
set M= the L_meet of 1L;
A1: M is idempotent & M is commutative associative
& M has_a_unity by LATTICE2:30,31,32,73;
thus FinMeet(f.:B,g) = M$$(f.:B,g) by LATTICE2:def 4
.= M$$(B,g*f) by A1,SETWISEO:44
.= FinMeet(B,g*f)by LATTICE2:def 4;
end;
theorem Th30:
FinMeet B1 "/\" FinMeet B2 = FinMeet (B1 \/ B2)
proof
set M= the L_meet of 1L;
A1: M is idempotent & M is commutative & M is associative
& M has_a_unity by LATTICE2:30,31,32,73;
thus FinMeet (B1 \/ B2) = M $$ (B1 \/ B2,id 1L) by Th14
.= M.(M $$ (B1,id 1L ),M $$ (B2,id 1L)) by A1,SETWISEO:42
.= M $$ (B1,id 1L) "/\" M $$ (B2,id 1L) by LATTICES:def 2
.= FinMeet B1 "/\" M $$ (B2,id 1L) by Th14
.=FinMeet B1 "/\" FinMeet B2 by Th14;
end;
theorem
Th31: for F being ClosedSubset of 1L st Top 1L in F
for B holds B c= F implies FinMeet B in F
proof
let F be ClosedSubset of 1L;
defpred X[Finite_Subset of the carrier of 1L] means
$1 c= F implies FinMeet $1 in F;
assume Top 1L in F;
then
A1: X[{}.the carrier of 1L] by Th26;
A2: for B1 being Finite_Subset of the carrier of 1L
for p being Element of 1L st X[B1]
holds X[B1 \/ {p}]
proof
let B1 be Finite_Subset of the carrier of 1L;
let p be Element of 1L;
assume A3:B1 c=F implies FinMeet B1 in F;
assume A4:B1 \/ {p} c=F;
then {p} c= F by XBOOLE_1:11;
then p in F by ZFMISC_1:37;
then FinMeet B1 "/\" p in F by A3,A4,Def10,XBOOLE_1:11;
hence thesis by Th28;
end;
thus for B being Element of Fin the carrier of 1L
holds X[B] from FinSubInd3(A1,A2);
end;
begin :: Distributive Upper-bounded Lattices
reserve DL for distributive upper-bounded Lattice,
B for Finite_Subset of the carrier of DL,
p for Element of DL,
f for UnOp of the carrier of DL;
Lm3: (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
set J = the L_join of DL;
set M = the L_meet of DL;
A1: M is idempotent & M is commutative & M is associative
by LATTICE2:30,31,32;
A2: J is_distributive_wrt M by LATTICE2:35;
now per cases;
suppose B<> {};
hence J.(M $$ (B,f),p) = M $$ (B,J [:] (f,p)) by A1,A2,SETWISEO:37;
suppose A3: B = {};
A4: now let f;
thus M $$ (B,f) = FinMeet({}.the carrier of DL,f) by A3,LATTICE2:
def 4
.=Top DL by Lm2;
end;
hence J.(M $$ (B,f),p) = J.(Top DL,p)
.= Top DL "\/" p by LATTICES:def 1
.= Top DL by LATTICES:44
.= M $$ (B,J [:] (f,p)) by A4;
end;
hence thesis;
end;
theorem
Th32: FinMeet B "\/" p = FinMeet (((the L_join of DL)[:](id DL,p)).:B)
proof
set J = the L_join of DL;
set M = the L_meet of DL;
thus FinMeet B "\/" p =J.(FinMeet B,p) by LATTICES:def 1
.= J.(M $$ (B,id DL),p) by Th14
.= M $$ (B,J [:] (id DL,p)) by Lm3
.=FinMeet(B,J [:] (id DL,p)) by LATTICE2:def 4
.= FinMeet (B,(id DL)*(J [:] (id DL,p))) by TMAP_1:93
.= FinMeet ((J [:] (id DL,p)).:B,id DL) by Th29
.= FinMeet (((the L_join of DL)[:](id DL,p)).:
B) by Def13;
end;
begin :: Implicative Lattices
reserve CL for C_Lattice;
reserve IL for implicative Lattice;
reserve f for Homomorphism of IL,CL;
reserve i,j,k for Element of IL;
theorem Th33:
f.i "/\" f.(i => j) [= f.j
proof
i "/\" (i => j) [= j by FILTER_0:def 8;
then f.(i "/\" (i => j)) [= f.j by Th7;
hence thesis by Def1;
end;
theorem Th34:
f is monomorphism implies (f.i "/\" f.k [= f.j implies f.k [= f.(i => j))
proof
assume A1: f is monomorphism;
hereby
assume f.i "/\" f.k [= f.j;
then f.(i "/\" k) [= f.j by Def1;
then i "/\" k [= j by A1,Th8;
then k [= (i => j) by FILTER_0:def 8;
hence f.k [= f.(i => j) by Th7;
end;
end;
theorem
f is isomorphism implies (CL is implicative & f preserves_implication)
proof
assume f is isomorphism;
then A1: f is epimorphism monomorphism by Def4;
thus CL is implicative
proof
let p,q be Element of CL;
consider i such that A2: f.i=p by A1,Th9;
consider j such that A3: f.j=q by A1,Th9;
take r = f.(i => j);
thus p "/\" r [= q by A2,A3,Th33;
hereby let r1 be Element of CL;
consider k such that
A4: f.k = r1 by A1,Th9;
assume p "/\" r1 [= q;
hence r1 [= r by A1,A2,A3,A4,Th34;
end;
end;
then reconsider CL as implicative Lattice;
reconsider f as Homomorphism of IL,CL;
now let i,j;
A5: (f.i) "/\" f.(i => j) [= (f.j) by Th33;
now let r1 be Element of CL;
consider k such that
A6:f.k=r1 by A1,Th9;
assume (f.i) "/\" r1 [= (f.j);
hence r1 [= f.(i => j) by A1,A6,Th34;
end;
hence (f.i) => (f.j) = f.(i => j) by A5,FILTER_0:def 8;
end;
hence thesis by Def6;
end;
begin ::Boolean Lattices
reserve BL for Boolean Lattice;
reserve f for Homomorphism of BL,CL;
reserve A for non empty Subset of BL;
reserve a1,a,b,c,p,q for Element of BL;
reserve B,B0,B1,B2,B3,A1,A2 for Finite_Subset of the carrier of BL;
theorem
Th36: (Top BL)`=Bottom BL
proof
set a=Bottom BL;
thus (Top BL)` = (a "\/" a`)` by LATTICES:48
.= a` "/\"a`` by LATTICES:51
.= Bottom BL by LATTICES:47;
end;
theorem
Th37: (Bottom BL)`=Top BL
proof
set a=Top BL;
thus (Bottom BL)` = (a "/\" a`)` by LATTICES:47
.= a` "\/"a`` by LATTICES:50
.= Top BL by LATTICES:48;
end;
theorem
f is epimorphism implies CL is Boolean & f preserves_complement
proof
assume A1: f is epimorphism;
then A2: f preserves_top by Th25;
A3: f preserves_bottom by A1,Th19;
thus CL is bounded complemented;
thus CL is distributive by A1,Th18;
then reconsider CL as Boolean Lattice by LATTICES:def 20;
reconsider f as Homomorphism of BL,CL;
now let a1;
A4: f.(a1`)"\/"f.a1 =f.(a1` "\/" a1) by Def1
.=f.(Top BL) by LATTICES:48
.= Top CL by A2,Def7;
f.(a1`)"/\"f.a1 = f.(a1` "/\" a1) by Def1
.=f.(Bottom BL) by LATTICES:47
.= Bottom CL by A3,Def8;
then f.(a1`) is_a_complement_of f.a1 by A4,LATTICES:def 18;
hence (f.a1)` = f.(a1`) by LATTICES:def 21;
end;
hence thesis by Def9;
end;
definition let BL;
mode Field of BL -> non empty Subset of BL means
:Def14: a in it & b in it implies a "/\" b in it & a` in it;
existence
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; thus thesis;
end;
end;
reserve F,H for Field of BL;
theorem
Th39: a in F & b in F implies a "\/" b in F
proof
assume a in F & b in F;
then a` in F & b` in F by Def14;
then a` "/\" b` in F by Def14;
then ( a"\/"b )` in F by LATTICES:51;
then ( a"\/"b )`` in F by Def14;
hence a"\/"b in F by LATTICES:49;
end;
theorem
Th40: a in F & b in F implies a => b in F
proof
assume A1: a in F & b in F;
then a` in F by Def14;
then a` "\/" b in F by A1,Th39;
hence a => b in F by FILTER_0:55;
end;
theorem
Th41: the carrier of BL is Field of BL
proof
the carrier of BL c= the carrier of BL;
then reconsider F=the carrier of BL as non empty Subset of BL;
a in F & b in F implies a "/\" b in F & a` in F;
hence the carrier of BL is Field of BL by Def14;
end;
theorem
Th42: F is ClosedSubset of BL
proof
for a,b st a in F & b in F holds
a "/\" b in F & a "\/" b in F by Def14,Th39;
hence F is ClosedSubset of BL by Def10;
end;
definition let BL,A;
func field_by A -> Field of BL means
:Def15: A c= it & for F st A c= F holds it c= F;
existence
proof
defpred X[set] means $1 is Field of BL & A c= $1;
consider X such that
A1: Z in X iff Z in bool the carrier of BL & X[Z] from Separation;
consider x being Element of A;
A2: the carrier of BL c= the carrier of BL;
reconsider x as Element of BL;
A3: A c= the carrier of BL & the carrier of BL is Field of BL &
the carrier of BL in bool the carrier of BL by A2,Th41;
then A4: the carrier of BL in X by A1;
A5: X <> {} by A1,A3;
now let Z;
assume Z in X;
then A c= Z by A1;
hence x in Z by TARSKI:def 3;
end;
then reconsider F1 = meet X as non empty set by A5,SETFAM_1:def 1;
F1 c= the carrier of BL
proof
let x;
thus thesis by A4,SETFAM_1:def 1;
end;
then reconsider F1 as non empty Subset of BL;
F1 is Field of BL
proof
let a,b;
assume A6: a in F1 & b in F1;
A7: a "/\" b in F1
proof
for Z st Z in X holds a "/\" b in Z
proof
let Z;
assume A8: Z in X;
then A9: Z is Field of BL by A1;
a in Z & b in Z by A6,A8,SETFAM_1:def 1;
hence thesis by A9,Def14;
end;
hence thesis by A5,SETFAM_1:def 1;
end;
a` in F1
proof
for Z st Z in X holds a` in Z
proof
let Z;
assume A10: Z in X;
then A11: Z is Field of BL by A1;
a in Z by A6,A10,SETFAM_1:def 1;
hence thesis by A11,Def14;
end;
hence thesis by A5,SETFAM_1:def 1;
end;
hence thesis by A7;
end;
then reconsider F = F1 as Field of BL;
take F;
for Z st Z in X holds A c= Z by A1;
hence A c= F by A4,SETFAM_1:6;
let H;
assume A c= H;
then H in X by A1;
hence F c= H by SETFAM_1:4;
end;
uniqueness
proof
let F1,F2 be Field of BL such that
A12: A c= F1 & for F st A c= F holds F1 c= F and
A13: A c= F2 & for F st A c= F holds F2 c= F;
thus F1 c= F2 & F2 c= F1 by A12,A13;
end;
end;
definition let BL,A;
func SetImp A -> Subset of BL equals
:Def16: { a => b : a in A & b in A};
coherence
proof
set B={ a => b : a in A & b in A};
B c= the carrier of BL
proof
let x;
assume x in B;
then ex p,q st x = p => q & p in A & q in A;
hence x in the carrier of BL;
end;
hence thesis;
end;
end;
definition let BL,A;
cluster SetImp A -> non empty;
coherence
proof
set B={ a => b : a in A & b in A};
consider x being Element of A;
reconsider x as Element of BL;
x => x in B;
then reconsider B as non empty set;
B = SetImp A by Def16;
hence thesis;
end;
end;
theorem
Th43: x in SetImp A iff ex p,q st x = p => q & p in A & q in A
proof
SetImp A = { a => b : a in A & b in A} by Def16;
hence thesis;
end;
theorem Th44: c in SetImp A iff ex p,q st c = p` "\/" q & p in A & q in A
proof
hereby assume c in SetImp A;
then consider p,q such that
A1: c = p => q & p in A & q in A by Th43;
take p,q;
thus c = p` "\/" q & p in A & q in A by A1,FILTER_0:55;
end;
given p,q such that
A2: c = p` "\/" q & p in A & q in A;
c = p => q by A2,FILTER_0:55;
hence c in SetImp A by A2,Th43;
end;
definition let BL;
deffunc U(Element of BL) = $1`;
func comp BL -> Function of the carrier of BL, the carrier of BL means
:Def17:
it.a = a`;
existence
proof
consider f being Function of the carrier of BL,the carrier of BL such that
A1: for a holds f.a= U(a) from LambdaD;
take f;
thus thesis by A1;
end;
uniqueness
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 = U(x)) &
(for x being Element of BL holds f2.x = U(x))
holds f1 = f2 from FuncDefUniq;
end;
end;
theorem Th45:
FinJoin(B \/ {b},comp BL) = FinJoin (B,comp BL) "\/" b`
proof
thus FinJoin(B \/ {b},comp BL) = FinJoin(B,comp BL) "\/" (comp BL).b by Th20
.= FinJoin (B,comp BL) "\/" b` by Def17;
end;
theorem
(FinJoin B)` = FinMeet (B,comp BL)
proof
set M= the L_meet of BL;
set J= the L_join of BL;
A1: M is idempotent commutative associative
& M has_a_unity by LATTICE2:30,31,32,73;
A2: J is idempotent commutative associative
& J has_a_unity by LATTICE2:26,27,29,67;
A3: (comp BL).(the_unity_wrt J) = the_unity_wrt M
proof
thus (comp BL).(the_unity_wrt J)= (the_unity_wrt J)` by Def17
.=(Bottom BL )` by LATTICE2:68
.=Top BL by Th37
.= the_unity_wrt M by LATTICE2:74;
end;
A4: for a,b being Element of BL
holds (comp BL).(J.(a,b))= M.((comp BL).a,(comp BL).b)
proof
let a,b be Element of BL;
thus (comp BL).(J.(a,b))=(comp BL).(a"\/"b) by LATTICES:def 1
.=(a"\/"b)` by Def17
.=a`"/\"b` by LATTICES:51
.=M.(a`,b`) by LATTICES:def 2
.= M.((comp BL).a,b`) by Def17
.= M.((comp BL).a,(comp BL).b) by Def17;
end;
thus (FinJoin B)`= (J$$(B,id BL))` by Th15
.= (comp BL).(J$$(B,id BL)) by Def17
.= M$$(B,(comp BL)*(id BL)) by A1,A2,A3,A4,SETWISEO:45
.= M$$(B, comp BL) by TMAP_1:93
.= FinMeet(B, comp BL) by LATTICE2:def 4;
end;
theorem
FinMeet(B \/ {b},comp BL) = FinMeet (B,comp BL) "/\" b`
proof
thus FinMeet(B \/ {b},comp BL) =FinMeet (B,comp BL) "/\" (comp BL).b by Th27
.=FinMeet (B,comp BL) "/\" b` by Def17;
end;
theorem Th48:
(FinMeet B)` = FinJoin (B,comp BL)
proof
set M= the L_meet of BL;
set J= the L_join of BL;
A1: M is idempotent commutative associative
& M has_a_unity by LATTICE2:30,31,32,73;
A2: J is idempotent commutative associative
& J has_a_unity by LATTICE2:26,27,29,67;
A3: (comp BL).(the_unity_wrt M) = the_unity_wrt J
proof
thus (comp BL).(the_unity_wrt M)= (the_unity_wrt M)` by Def17
.=(Top BL )` by LATTICE2:74
.=Bottom BL by Th36
.= the_unity_wrt J by LATTICE2:68;
end;
A4: for a,b being Element of BL
holds (comp BL).(M.(a,b))= J.((comp BL).a,(comp BL).b)
proof
let a,b be Element of BL;
thus (comp BL).(M.(a,b))=(comp BL).(a"/\"b) by LATTICES:def 2
.=(a"/\"b)` by Def17
.=a`"\/"b` by LATTICES:50
.=J.(a`,b`) by LATTICES:def 1
.= J.((comp BL).a,b`) by Def17
.= J.((comp BL).a,(comp BL).b) by Def17;
end;
thus (FinMeet B)`= (M$$(B,id BL))` by Th14
.= (comp BL).(M$$(B,id BL)) by Def17
.= J$$(B,(comp BL)*(id BL)) by A1,A2,A3,A4,SETWISEO:45
.= J$$(B, comp BL) by TMAP_1:93
.= FinJoin(B, comp BL) by LATTICE2:def 3;
end;
theorem
Th49: for AF being non empty ClosedSubset of BL st Bottom
BL in AF & Top BL in AF
for B holds B c= SetImp AF implies
ex B0 st B0 c= SetImp AF & FinJoin( B,comp BL) = FinMeet B0
proof
let AF be non empty ClosedSubset of BL such that A1:Bottom BL in AF & Top
BL in AF;
let B;
assume A2: B c= SetImp AF;
set C={ FinJoin A1 "\/" FinJoin(A2,comp BL): A1 c= AF & A2 c= AF};
defpred X[Finite_Subset of the carrier of BL] means
$1 c= SetImp AF implies
ex B0 st B0 c= C & FinJoin($1,comp BL) = FinMeet B0;
A3: X[{}.the carrier of BL]
proof
assume {}.the carrier of BL c= SetImp AF;
take B0={Bottom BL};
A4: FinJoin ({}.the carrier of BL,comp BL)= Bottom BL by Lm1
.=FinMeet {Bottom BL} by Th17;
B0 c= C
proof
let x;
assume x in B0;
then A5: x = Bottom BL by TARSKI:def 1;
ex A1,A2 st
x = FinJoin A1 "\/" FinJoin(A2,comp BL) & A1 c= AF & A2 c= AF
proof
take A1={Bottom BL};
take A2={Top BL};
thus x = Bottom BL "\/" Bottom BL by A5,LATTICES:17
.= Bottom BL "\/" (Top BL)` by Th36
.=FinJoin A1 "\/" (Top BL)` by Th16
.=FinJoin A1 "\/" (FinMeet A2)` by Th17
.=FinJoin A1 "\/" FinJoin (A2,comp BL) by Th48;
thus A1 c= AF by A1,ZFMISC_1:37;
thus A2 c= AF by A1,ZFMISC_1:37;
end;
hence x in C;
end;
hence thesis by A4;
end;
A6: for B' being Finite_Subset of the carrier of BL,
b being Element of BL st X[B']
holds X[B' \/ {b}]
proof
let B' be Finite_Subset of the carrier of BL,
b be Element of BL;
assume A7: (B' c= SetImp AF implies
ex B1 st B1 c= C & FinJoin(B',comp BL) = FinMeet B1 );
assume A8: B' \/ {b} c= SetImp AF;
then A9: B' c= SetImp AF & b in SetImp AF by SETWISEO:8;
consider B1 such that
A10: B1 c= C & FinJoin(B',comp BL) = FinMeet B1 by A7,A8,SETWISEO:8;
consider p,q such that
A11: b = p` "\/" q & p in AF & q in AF by A9,Th44;
A12: b` = p`` "/\" q` by A11,LATTICES:51
.= p "/\" q` by LATTICES:49;
set J = the L_join of BL;
take (J[:](id BL,p)).:B1 \/ (J[:](id BL,q`)).:B1;
A13: FinJoin(B' \/ {b} ,comp BL) = FinMeet B1 "\/" (p "/\"
q`) by A10,A12,Th45
.= (FinMeet B1 "\/" p) "/\" (FinMeet B1 "\/" q`) by LATTICES:31
.= FinMeet((J[:](id BL,p)).:B1) "/\" (FinMeet B1 "\/" q`) by Th32
.= FinMeet((J[:](id BL,p)).:B1) "/\" FinMeet ((J[:]
(id BL,q`)).:B1) by Th32
.= FinMeet ((J[:](id BL,p)).:B1 \/ (J[:](id BL,q`)).:B1) by Th30;
A14: for x,b holds x in (J[:](id BL,b)).:B1 implies ex a st
a in B1 & x = a "\/" b
proof
let x,b;
assume A15: x in (J[:](id BL,b)).:B1;
(J[:](id BL,b)).:B1 c= the carrier of BL by FUNCT_2:44;
then reconsider x as Element of BL by A15;
consider a such that
A16: a in B1 & x = (J[:](id BL,b)).a by A15,FUNCT_2:116;
x = J.(id BL.a,b) by A16,FUNCOP_1:60
.= J.(a,b) by TMAP_1:91
.= a "\/" b by LATTICES:def 1;
hence thesis by A16;
end;
A17: (J[:](id BL,p)).:B1 c= C
proof
let x;
assume x in (J[:](id BL,p)).:B1;
then consider a such that
A18: a in B1 & x = a "\/" p by A14;
a in C by A10,A18;
then consider A1,A2 such that
A19: a = FinJoin A1 "\/" FinJoin(A2,comp BL) & A1 c= AF & A2 c= AF;
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'=A1 \/ {p};
take A2'=A2;
x = (FinJoin A1 "\/" p) "\/" FinJoin(A2,comp BL) by A18,A19,
LATTICES:def 5
.= FinJoin(A1') "\/" FinJoin(A2',comp BL) by Th21;
hence thesis by A11,A19,SETWISEO:8;
end;
hence x in C;
end;
(J[:](id BL,q`)).:B1 c= C
proof
let x;
assume x in (J[:](id BL,q`)).:B1;
then consider a such that
A20: a in B1 & x = a "\/" q` by A14;
a in C by A10,A20;
then consider A1,A2 such that
A21: a = FinJoin A1 "\/" FinJoin(A2,comp BL) & A1 c= AF & A2 c= AF;
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'=A1;
take A2'=A2 \/ {q};
x = FinJoin A1 "\/" (FinJoin(A2,comp BL) "\/" q`) by A20,A21,
LATTICES:def 5
.= FinJoin(A1') "\/" FinJoin(A2',comp BL) by Th45;
hence thesis by A11,A21,SETWISEO:8;
end;
hence x in C;
end;
hence thesis by A13,A17,XBOOLE_1:8;
end;
for B being Finite_Subset of the carrier of BL holds X[B]
from FinSubInd3(A3,A6
);
then consider B1 such that
A22: B1 c= C & FinJoin(B,comp BL) = FinMeet B1 by A2;
C c= SetImp AF
proof
let x;
assume x in C;
then consider A1,A2 such that
A23: x = FinJoin A1 "\/" FinJoin(A2,comp BL) & A1 c= AF & A2 c= AF;
consider p,q such that
A24: p = FinMeet A2 & q = FinJoin A1;
A25: p in AF & q in AF by A1,A23,A24,Th24,Th31;
x = p` "\/" q by A23,A24,Th48;
hence x in SetImp AF by A25,Th44;
end;
then B1 c= SetImp AF by A22,XBOOLE_1:1;
hence thesis by A22;
end;
theorem
for AF being non empty ClosedSubset of BL st Bottom
BL in AF & Top BL in AF holds
{ FinMeet B : B c= SetImp AF } = field_by AF
proof
let AF be non empty ClosedSubset of BL such that
A1: Bottom BL in AF & Top BL in AF;
set A1= { FinMeet B :B c= SetImp AF };
A2: AF c= A1
proof
let x;
assume A3:x in AF;
then reconsider b=x as Element of BL;
reconsider B = {b} as Finite_Subset of the carrier of BL;
b = Bottom BL "\/" b by LATTICES:39
.= (Top BL)` "\/" b by Th36;
then b in SetImp AF by A1,A3,Th44;
then A4: B c= SetImp AF by ZFMISC_1:37;
x = FinMeet B by Th17;
hence x in A1 by A4;
end;
A1 c= the carrier of BL
proof
let x;
assume x in A1;
then consider B such that
A5: x = FinMeet B & B c= SetImp AF;
thus x in the carrier of BL by A5;
end;
then reconsider A1 as non empty Subset of BL by A1,A2;
A6: A1 is Field of BL
proof
let p,q;
assume A7: p in A1 & q in A1;
thus p "/\" q in A1
proof
consider B1 such that
A8: p=FinMeet B1 & B1 c= SetImp AF by A7;
consider B2 such that
A9: q=FinMeet B2 & B2 c= SetImp AF by A7;
consider B0 such that
A10: B0=B1 \/ B2;
A11: B0 c= SetImp AF by A8,A9,A10,XBOOLE_1:8;
p "/\" q = FinMeet B0 by A8,A9,A10,Th30;
hence thesis by A11;
end;
thus p` in A1
proof
consider B such that
A12: p=FinMeet B & B c= SetImp AF by A7;
p` = FinJoin ( B,comp BL) by A12,Th48;
then consider B0 such that
A13: B0 c= SetImp AF & p` = FinMeet B0 by A1,A12,Th49;
thus thesis by A13;
end;
end;
now let F;
assume A14: AF c= F;
thus A1 c= F
proof
let x;
assume x in A1;
then consider B such that
A15: x=FinMeet B & B c= SetImp AF;
A16: SetImp AF c= F
proof
let y;
assume y in SetImp AF;
then consider p,q such that
A17: y = p => q & p in AF & q in AF by Th43;
thus y in F by A14,A17,Th40;
end;
reconsider F1=F as ClosedSubset of BL by Th42;
B c= F1 & Top BL in F1 by A1,A14,A15,A16,XBOOLE_1:1;
hence x in F by A15,Th31;
end;
end;
hence thesis by A2,A6,Def15;
end;