:: Representation Theorem for Boolean Algebras
:: by Jaros{\l}aw Stanis{\l}aw Walijewski
::
:: Received July 14, 1993
:: Copyright (c) 1993-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, PRE_TOPC, SUBSET_1, SETFAM_1, RCOMP_1, TARSKI,
ZFMISC_1, STRUCT_0, BINOP_1, FUNCT_1, LATTICES, EQREL_1, XXREAL_2,
CARD_FIL, RELAT_1, INT_2, FINSUB_1, SETWISEO, FILTER_0, LATTICE2, PBOOLE,
FINSET_1, CLASSES1, CARD_1, GROUP_6, FUNCT_2, WELLORD1, LOPCLSET,
LATTICE4;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, RELSET_1,
PARTFUN1, FUNCT_2, BINOP_1, FINSUB_1, STRUCT_0, PRE_TOPC, LATTICES,
LATTICE2, FILTER_0, FINSET_1, SETWISEO, LATTICE4, CLASSES1, CARD_1;
constructors BINOP_1, SETWISEO, PRE_TOPC, LATTICE2, FILTER_1, CLASSES1,
LATTICE4, RELSET_1, FILTER_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FINSET_1,
FINSUB_1, STRUCT_0, LATTICES, PRE_TOPC, CARD_1, RELSET_1, TOPS_1,
LATTICE2;
requirements BOOLE, SUBSET;
definitions TARSKI, LATTICES, BINOP_1, STRUCT_0, XBOOLE_0;
equalities LATTICES, STRUCT_0, SUBSET_1;
expansions TARSKI, LATTICES, XBOOLE_0;
theorems TARSKI, SETFAM_1, LATTICES, FINSUB_1, TOPS_1, PRE_TOPC, SUBSET_1,
LATTICE2, LATTICE4, FILTER_0, FUNCT_1, FUNCT_2, ZFMISC_1, GROUP_6,
SETWISEO, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, STRUCT_0, CLASSES1,
EQREL_1;
schemes BINOP_1, FRAENKEL, FUNCT_1, SETWISEO, BINOP_2;
begin
reserve T for non empty TopSpace,
X,Z for Subset of T;
definition
let T be non empty TopStruct;
func OpenClosedSet(T) -> Subset-Family of T equals
{x where x is Subset of T: x is open closed};
coherence
proof
set A= {x where x is Subset of T: x is open closed};
A c= bool the carrier of T
proof
let y be object;
assume y in A;
then ex x being Subset of T st y=x & x is open & x is closed;
hence thesis;
end;
hence thesis;
end;
end;
registration
let T be non empty TopSpace;
cluster OpenClosedSet(T) -> non empty;
coherence
proof
set A= {x where x is Subset of T : x is open closed};
{} T in A;
hence thesis;
end;
end;
theorem Th1:
X in OpenClosedSet(T) implies X is open
proof
assume X in OpenClosedSet(T);
then ex Z st Z=X & Z is open & Z is closed;
hence thesis;
end;
theorem Th2:
X in OpenClosedSet(T) implies X is closed
proof
assume X in OpenClosedSet(T);
then ex Z st Z=X & Z is open & Z is closed;
hence thesis;
end;
theorem Th3:
X is open closed implies X in OpenClosedSet(T);
reserve x,y for Element of OpenClosedSet(T);
definition
let T;
let C,D be Element of OpenClosedSet(T);
redefine func C \/ D -> Element of OpenClosedSet(T); :: redefines \/ (XBOOLE_0, definition)
coherence
proof
reconsider A = C, B = D as Subset of T;
A1: A is open by Th1;
A2: B is open by Th1;
A3: A is closed by Th2;
A4: B is closed by Th2;
A \/ B is open by A1,A2;
hence C \/ D is Element of OpenClosedSet(T) by A3,A4,Th3;
end;
redefine func C /\ D -> Element of OpenClosedSet(T); :: redefines /\ (XBOOLE_0, definition)
coherence
proof
reconsider A = C, B = D as Subset of T;
A5: A is open by Th1;
A6: B is open by Th1;
A7: A is closed by Th2;
A8: B is closed by Th2;
A /\ B is open by A5,A6;
hence C /\ D is Element of OpenClosedSet(T) by A7,A8,Th3;
end;
end;
definition
let T;
deffunc U(Element of OpenClosedSet(T),Element of OpenClosedSet(T))
= $1 \/ $2;
func T_join T -> BinOp of OpenClosedSet(T) means
:Def2:
for A,B being Element of OpenClosedSet(T) holds it.(A,B) = A \/ B;
existence
proof
consider f being BinOp of OpenClosedSet(T) such that
A1: for x,y being Element of OpenClosedSet(T) holds
f.(x,y)= U(x,y) from BINOP_1:sch 4;
take f;
let x,y;
thus thesis by A1;
end;
uniqueness
proof
thus for b1,b2 being BinOp of OpenClosedSet(T) st
(for A,B being Element of OpenClosedSet(T) holds b1.(A,B) = U(A,B)) &
(for A,B being Element of OpenClosedSet(T) holds b2.(A,B) = U(A,B))
holds b1 = b2 from BINOP_2:sch 2;
end;
deffunc U(Element of OpenClosedSet(T),Element of OpenClosedSet(T))
= $1 /\ $2;
func T_meet T -> BinOp of OpenClosedSet(T) means
:Def3:
for A,B being Element of OpenClosedSet(T) holds it.(A,B) = A /\ B;
existence
proof
consider f being BinOp of OpenClosedSet(T) such that
A2: for x,y being Element of OpenClosedSet(T) holds
f.(x,y)= U(x,y) from BINOP_1:sch 4;
take f;
let x,y;
thus thesis by A2;
end;
uniqueness
proof
thus for b1,b2 being BinOp of OpenClosedSet(T) st
(for A,B being Element of OpenClosedSet(T) holds b1.(A,B) = U(A,B)) &
(for A,B being Element of OpenClosedSet(T) holds b2.(A,B) = U(A,B))
holds b1 = b2 from BINOP_2:sch 2;
end;
end;
theorem
for x,y be Element of LattStr(#OpenClosedSet(T),T_join T,T_meet T#),
x9,y9 be Element of OpenClosedSet(T)
st x=x9 & y=y9 holds x"\/"y = x9 \/ y9 by Def2;
theorem
for x,y be Element of LattStr(#OpenClosedSet(T),T_join T,T_meet T#),
x9,y9 be Element of OpenClosedSet(T)
st x=x9 & y=y9 holds x"/\"y = x9 /\ y9 by Def3;
theorem
{} T is Element of OpenClosedSet(T) by Th3;
theorem
[#] T is Element of OpenClosedSet(T) by Th3;
theorem Th8:
x` is Element of OpenClosedSet(T)
proof
reconsider y = x as Subset of T;
A1: y is open by Th1;
y is closed by Th2;
then
A2: x` is open;
x` is closed by A1;
hence thesis by A2,Th3;
end;
theorem Th9:
LattStr(#OpenClosedSet(T),T_join T,T_meet T#) is Lattice
proof
set L = LattStr(#OpenClosedSet(T),T_join T,T_meet T#);
A1: for p,q be Element of L holds p"\/"q = q"\/"p
proof
let p,q be Element of L;
consider p9,q9 being Element of OpenClosedSet(T) such that
A2: p=p9 and
A3: q=q9;
thus p "\/" q = q9 \/ p9 by A2,A3,Def2
.= q"\/"p by A2,A3,Def2;
end;
A4: for p,q,r be Element of L holds p"\/"(q"\/"r) = (p"\/"q)"\/"r
proof
let p,q,r be Element of L;
consider p9,q9,r9,k9,l9 being Element of OpenClosedSet(T) such that
A5: p=p9 and
A6: q=q9 and
A7: r=r9 and
A8: q "\/" r=k9 and
A9: p "\/" q=l9;
thus p"\/"(q"\/"r) = p9 \/ k9 by A5,A8,Def2
.= p9 \/ (q9 \/ r9) by A6,A7,A8,Def2
.= (p9 \/ q9) \/ r9 by XBOOLE_1:4
.= l9 \/ r9 by A5,A6,A9,Def2
.= (p"\/"q)"\/"r by A7,A9,Def2;
end;
A10: for p,q be Element of L holds (p"/\"q)"\/"q = q
proof
let p,q be Element of L;
consider p9,q9,k9 being Element of OpenClosedSet(T) such that
A11: p=p9 and
A12: q=q9 and
A13: p"/\"q=k9;
thus (p"/\"q)"\/"q = k9 \/ q9 by A12,A13,Def2
.= (p9 /\ q9) \/ q9 by A11,A12,A13,Def3
.= q by A12,XBOOLE_1:22;
end;
A14: for p,q be Element of L holds p"/\"q = q"/\"p
proof
let p,q be Element of L;
consider p9,q9 being Element of OpenClosedSet(T) such that
A15: p=p9 and
A16: q=q9;
thus p "/\" q =q9 /\ p9 by A15,A16,Def3
.= q"/\"p by A15,A16,Def3;
end;
A17: for p,q,r be Element of L holds p"/\"(q"/\"r) = (p"/\"q)"/\"r
proof
let p,q,r be Element of L;
consider p9,q9,r9,k9,l9 being Element of OpenClosedSet(T) such that
A18: p=p9 and
A19: q=q9 and
A20: r=r9 and
A21: q "/\" r=k9 and
A22: p "/\" q=l9;
thus p"/\"(q"/\"r) = p9 /\ k9 by A18,A21,Def3
.= p9 /\ (q9 /\ r9) by A19,A20,A21,Def3
.= (p9 /\ q9) /\ r9 by XBOOLE_1:16
.= l9 /\ r9 by A18,A19,A22,Def3
.= (p"/\"q)"/\"r by A20,A22,Def3;
end;
for p,q be Element of L holds p"/\"(p"\/"q)=p
proof
let p,q be Element of L;
consider p9,q9,k9 being Element of OpenClosedSet(T) such that
A23: p=p9 and
A24: q=q9 and
A25: p"\/"q=k9;
thus p"/\"(p"\/"q) = p9 /\ k9 by A23,A25,Def3
.= p9 /\ (p9 \/ q9) by A23,A24,A25,Def2
.= p by A23,XBOOLE_1:21;
end;
then L is join-commutative join-associative meet-absorbing
meet-commutative meet-associative join-absorbing
by A1,A4,A10,A14,A17;
hence thesis;
end;
definition
let T be non empty TopSpace;
func OpenClosedSetLatt(T) -> Lattice equals
LattStr(#OpenClosedSet(T),T_join T,T_meet T#);
coherence by Th9;
end;
theorem
for T being non empty TopSpace, x,y being Element of
OpenClosedSetLatt(T) holds x"\/"y = x \/ y by Def2;
theorem
for T being non empty TopSpace , x,y being Element of
OpenClosedSetLatt(T) holds x"/\"y = x /\ y by Def3;
theorem
the carrier of OpenClosedSetLatt(T) = OpenClosedSet(T);
registration
let T;
cluster OpenClosedSetLatt(T) -> Boolean;
coherence
proof
set OCL=OpenClosedSetLatt(T);
A1: for a,b,c being Element of OCL holds a"/\"(b"\/"c) = (a"/\"b)"\/"(a"/\"c)
proof
let a,b,c be Element of OCL;
set m = a"/\"c;
consider a9,b9,c9,k9,l9,m9 being Element of OpenClosedSet(T) such that
A2: a=a9 and
A3: b=b9 and
A4: c = c9 and
A5: b "\/" c = k9 and
A6: a"/\"b=l9 and
A7: m=m9;
A8: a9 /\ c9= m by A2,A4,Def3;
thus a"/\"(b"\/"c) =a9 /\ k9 by A2,A5,Def3
.= a9 /\ (b9 \/ c9) by A3,A4,A5,Def2
.= (a9 /\ b9) \/ (a9 /\ c9) by XBOOLE_1:23
.= l9 \/ m9 by A2,A3,A6,A7,A8,Def3
.= (a"/\"b)"\/"(a"/\"c) by A6,A7,Def2;
end;
reconsider bot = {} T as Element of OCL by Th3;
reconsider top = [#] T as Element of OCL by Th3;
A9: for a being Element of OCL holds top"\/"a =top & a "\/" top =top
proof
let a be Element of OCL;
reconsider a9 = a as Element of OpenClosedSet(T);
thus top "\/" a = [#] T \/ a9 by Def2
.= top by XBOOLE_1:12;
hence thesis;
end;
A10: for a being Element of OCL holds bot"/\"a = bot & a"/\"bot = bot
proof
let a be Element of OCL;
reconsider a9 = a as Element of OpenClosedSet(T);
thus bot "/\" a = {} /\ a9 by Def3
.= bot;
hence thesis;
end;
then
A11: OCL is lower-bounded;
A12: OCL is upper-bounded by A9;
A13: {} T= Bottom OCL by A10,A11,LATTICES:def 16;
A14: [#](T) = Top OCL by A9,A12,LATTICES:def 17;
thus OCL is bounded by A11,A12;
reconsider OCL as 01_Lattice by A11,A12;
for b being Element of OCL ex a being Element of OCL
st a is_a_complement_of b
proof
let b be Element of OCL;
reconsider c = b as Element of OpenClosedSet(T);
reconsider a = c` as Element of OCL by Th8;
A15: a"\/"b=c \/ c` by Def2
.=Top OCL by A14,PRE_TOPC:2;
A16: c misses c` by XBOOLE_1:79;
A17: a"/\"b = c /\ c` by Def3
.= Bottom OCL by A13,A16;
take a;
a"\/"b = b"\/"a & a"/\"b = b"/\"a;
hence thesis by A15,A17;
end;
hence thesis by A1;
end;
end;
theorem
[#] T is Element of OpenClosedSetLatt(T) by Th3;
theorem
{} T is Element of OpenClosedSetLatt(T) by Th3;
reserve x,y,X for set;
registration
cluster non trivial for B_Lattice;
existence
proof
set T = the non empty TopSpace;
reconsider E = OpenClosedSetLatt(T) as B_Lattice;
reconsider a = [#] T, b = {} T as Element of E by Th3;
take E,a,b;
thus thesis;
end;
end;
reserve BL for non trivial B_Lattice,
a,b,c,p,q for Element of BL,
UF,F,F0,F1,F2 for Filter of BL;
definition
let BL;
func ultraset BL -> Subset-Family of BL equals
{F : F is being_ultrafilter};
coherence
proof
set US = {F: F is being_ultrafilter};
US c= bool the carrier of BL
proof
let x be object;
assume x in US;
then ex UF st ( UF = x)&( UF is being_ultrafilter);
hence thesis;
end;
hence thesis;
end;
end;
registration
let BL;
cluster ultraset BL -> non empty;
coherence
proof
set US = {F: F is being_ultrafilter};
consider p1,p2 being Element of BL such that
A1: p1<>p2 by STRUCT_0:def 10;
p1 <> Bottom BL or p2 <> Bottom BL by A1;
then consider p being Element of BL such that
A2: p<>Bottom BL;
consider H being Filter of BL such that
p in H and
A3: H is being_ultrafilter by A2,FILTER_0:20;
H in US by A3;
hence thesis;
end;
end;
theorem
x in ultraset BL iff ex UF st UF = x & UF is being_ultrafilter;
theorem Th16:
for a holds { F :F is being_ultrafilter & a in F} c= ultraset BL
proof
let a;
let x be object;
assume x in { F :F is being_ultrafilter & a in F};
then ex UF st ( UF = x)&( UF is being_ultrafilter)&( a in UF);
hence thesis;
end;
definition
let BL;
func UFilter BL -> Function means
:Def6:
dom it = the carrier of BL & for a being Element of BL
holds it.a = {UF: UF is being_ultrafilter & a in UF };
existence
proof
deffunc U(object) = { F :F is being_ultrafilter & $1 in F};
consider f being Function such that
A1: dom f = the carrier of BL and
A2: for x being object st x in the carrier of BL
holds f.x = U(x) from FUNCT_1:sch 3;
take f;
thus thesis by A1,A2;
end;
uniqueness
proof
let f1,f2 be Function;
assume that
A3: dom f1= the carrier of BL &
for a holds f1.a={F: F is being_ultrafilter & a in F } and
A4: dom f2= the carrier of BL &
for a holds f2.a={F: F is being_ultrafilter & a in F };
now
let x be object;
assume x in the carrier of BL;
then reconsider a = x as Element of BL;
thus f1.x = {F: F is being_ultrafilter & a in F } by A3
.= f2.x by A4;
end;
hence thesis by A3,A4,FUNCT_1:2;
end;
end;
theorem Th17:
x in UFilter BL.a iff ex F st F=x & F is being_ultrafilter & a in F
proof
A1: x in UFilter BL.a implies ex F st F=x & F is being_ultrafilter & a in F
proof
assume x in UFilter BL.a;
then x in {UF: UF is being_ultrafilter & a in UF} by Def6;
then consider F such that
A2: F=x and
A3: F is being_ultrafilter and
A4: a in F;
take F;
thus thesis by A2,A3,A4;
end;
(ex F st F=x & F is being_ultrafilter & a in F) implies x in UFilter BL.a
proof
assume ex F st F=x & F is being_ultrafilter & a in F;
then x in {UF: UF is being_ultrafilter & a in UF};
hence thesis by Def6;
end;
hence thesis by A1;
end;
theorem Th18:
F in UFilter BL.a iff F is being_ultrafilter & a in F
proof
hereby
assume F in UFilter BL.a;
then ex F0 st ( F0=F)&( F0 is being_ultrafilter)&( a in F0) by Th17;
hence F is being_ultrafilter & a in F;
end;
thus thesis by Th17;
end;
theorem Th19:
for F st F is being_ultrafilter holds a "\/" b in F iff a in F or b in F
proof
let F;
assume F is being_ultrafilter;
then F is prime by FILTER_0:45;
hence thesis by FILTER_0:def 5;
end;
theorem Th20:
UFilter BL.(a "/\" b) = UFilter BL.a /\ UFilter BL.b
proof
A1: UFilter BL.(a "/\" b) c= UFilter BL.a /\ UFilter BL.b
proof
let x be object;
set c = a "/\" b;
assume x in UFilter BL.c;
then consider F0 such that
A2: x=F0 and
A3: F0 is being_ultrafilter and
A4: c in F0 by Th17;
A5: a in F0 by A4,FILTER_0:8;
A6: b in F0 by A4,FILTER_0:8;
A7: F0 in UFilter BL.(a) by A3,A5,Th17;
F0 in UFilter BL.(b) by A3,A6,Th17;
hence thesis by A2,A7,XBOOLE_0:def 4;
end;
UFilter BL.a /\ UFilter BL.b c= UFilter BL.(a "/\" b)
proof
let x be object;
assume
A8: x in UFilter BL.a /\ UFilter BL.b;
then
A9: x in UFilter BL.a by XBOOLE_0:def 4;
A10: x in UFilter BL.b by A8,XBOOLE_0:def 4;
A11: ex F0 st x=F0 & F0 is being_ultrafilter & a in F0 by A9,Th17;
ex F0 st x=F0 & F0 is being_ultrafilter & b in F0 by A10,Th17;
then consider F0 such that
A12: x=F0 and
A13: F0 is being_ultrafilter and
A14: a in F0 and
A15: b in F0 by A11;
a "/\" b in F0 by A14,A15,FILTER_0:8;
hence thesis by A12,A13,Th17;
end;
hence thesis by A1;
end;
theorem Th21:
UFilter BL.(a "\/" b) = UFilter BL.a \/ UFilter BL.b
proof
A1: UFilter BL.(a "\/" b) c= UFilter BL.a \/ UFilter BL.b
proof
let x be object;
set c = a "\/" b;
assume x in UFilter BL.c;
then consider F0 such that
A2: x=F0 and
A3: F0 is being_ultrafilter and
A4: c in F0 by Th17;
a in F0 or b in F0 by A3,A4,Th19;
then F0 in UFilter BL.(a) or F0 in UFilter BL.(b) by A3,Th17;
hence thesis by A2,XBOOLE_0:def 3;
end;
UFilter BL.a \/ UFilter BL.b c= UFilter BL.(a "\/" b)
proof
let x be object;
assume x in UFilter BL.a \/ UFilter BL.b;
then x in UFilter BL.a or x in UFilter BL.b by XBOOLE_0:def 3;
then ( ex F0 st x=F0 & F0 is being_ultrafilter & a in F0 ) or
ex F0 st x=F0 & F0 is being_ultrafilter & b in F0 by Th17;
then consider F0 such that
A5: x=F0 and
A6: F0 is being_ultrafilter and
A7: a in F0 or b in F0;
a "\/" b in F0 by A6,A7,Th19;
hence thesis by A5,A6,Th17;
end;
hence thesis by A1;
end;
definition
let BL;
redefine func UFilter BL -> Function of the carrier of BL, bool ultraset BL; :: redefines UFilter (LOPCLSET, definition)
coherence
proof
reconsider f=UFilter BL as Function;
A1: dom f = the carrier of BL by Def6;
rng f c= bool ultraset BL
proof
let y be object;
reconsider yy=y as set by TARSKI:1;
assume y in rng f;
then consider x being object such that
A2: x in dom f and
A3: y = f.x by FUNCT_1:def 3;
y ={F: F is being_ultrafilter & x in F} by A1,A2,A3,Def6;
then yy c= ultraset BL by A1,A2,Th16;
hence thesis;
end;
then reconsider f as Function of the carrier of BL, bool ultraset BL
by A1,FUNCT_2:def 1,RELSET_1:4;
for a holds f.a = { F :F is being_ultrafilter & a in F} by Def6;
hence thesis;
end;
end;
definition
let BL;
func StoneR BL -> set equals
rng UFilter BL;
coherence;
end;
registration
let BL;
cluster StoneR BL -> non empty;
coherence;
end;
theorem
StoneR BL c= bool ultraset BL;
theorem Th23:
x in StoneR BL iff ex a st (UFilter BL).a =x
proof
A1: x in StoneR BL implies ex a st (UFilter BL).a =x
proof
assume x in StoneR BL;
then consider y being object such that
A2: y in dom UFilter BL and
A3: x = UFilter BL.y by FUNCT_1:def 3;
reconsider a=y as Element of BL by A2;
take a;
thus thesis by A3;
end;
( ex a st UFilter BL.a =x ) implies x in StoneR BL
proof
given a such that
A4: x=UFilter BL.a;
a in the carrier of BL;
then a in dom UFilter BL by Def6;
hence thesis by A4,FUNCT_1:def 3;
end;
hence thesis by A1;
end;
definition
let BL;
func StoneSpace BL -> strict TopSpace means
:Def8:
the carrier of it =ultraset BL & the topology of it =
{union A where A is Subset-Family of ultraset BL : A c= StoneR BL };
existence
proof
set US = ultraset BL;
set STP={union A where A is Subset-Family of ultraset BL :
A c= StoneR BL };
STP c= bool US
proof
let x be object;
assume x in STP;
then ex B being Subset-Family of ultraset BL st ( x=union B)&( B
c= StoneR BL);
hence thesis;
end;
then reconsider STP ={union A where A is Subset-Family of ultraset BL :
A c= StoneR BL } as Subset-Family of US;
TopStruct(# US,STP#) is strict TopSpace
proof
set TS= TopStruct(# US,STP#);
A1: the carrier of TS in the topology of TS
proof
set B = { F : F is being_ultrafilter & Top BL in F };
B c= ultraset BL
proof
let x be object;
assume x in B;
then ex F st F= x & F is being_ultrafilter & Top BL in F;
hence thesis;
end;
then
A2: bool B c= bool ultraset BL by ZFMISC_1:67;
{B} c= bool B by ZFMISC_1:68;
then reconsider SB ={B} as
Subset-Family of ultraset BL by A2,XBOOLE_1:1;
reconsider SB as Subset-Family of ultraset BL;
A3: union SB = B by ZFMISC_1:25;
ultraset BL c= B
proof
let x be object;
assume x in ultraset BL;
then consider F such that
A4: F = x and
A5: F is being_ultrafilter;
Top BL in F by FILTER_0:11;
hence thesis by A4,A5;
end;
then
A6: ultraset BL = union SB by A3;
(UFilter BL).Top BL = { F : F is being_ultrafilter & Top BL in F }
by Def6;
then B in StoneR BL by Th23;
then SB c= StoneR BL by ZFMISC_1:31;
hence thesis by A6;
end;
A7: for a being Subset-Family of TS
st a c= the topology of TS holds union a in the topology of TS
proof
let a be Subset-Family of TS;
assume
A8: a c= the topology of TS;
set B= { A where A is Subset of StoneR BL : union A in a};
B c= bool StoneR BL
proof
let x be object;
assume x in B;
then ex C being Subset of StoneR BL st C = x & union C in a;
then reconsider C = x as Subset of StoneR BL;
C c= StoneR BL;
hence thesis;
end;
then reconsider BS=B as Subset-Family of StoneR BL;
A9: union union BS = union {union A where A
is Subset of StoneR BL :A in BS} by EQREL_1:54;
A10: a c= {union A where A is Subset of StoneR BL :A in BS}
proof
let x be object;
assume
A11: x in a;
then x in STP by A8;
then consider C being Subset-Family of ultraset BL such that
A12: x=union C and
A13: C c= StoneR BL;
C in BS by A11,A12,A13;
hence thesis by A12;
end;
{union A where A is Subset of StoneR BL :A in BS} c= a
proof
let x be object;
assume x in {union A where A is Subset of StoneR BL :A in BS};
then consider C being Subset of StoneR BL such that
A14: union C= x and
A15: C in BS;
ex D being Subset of StoneR BL st ( D = C)&( union D in a) by A15;
hence thesis by A14;
end;
then
A16: a = { union A where A is Subset of StoneR BL :A in BS} by A10;
union BS is Subset-Family of ultraset BL by XBOOLE_1:1;
hence thesis by A9,A16;
end;
for p,q being Subset of TS st
p in the topology of TS & q in the topology of TS
holds p /\ q in the topology of TS
proof
let p,q be Subset of TS;
assume that
A17: p in the topology of TS and
A18: q in the topology of TS;
consider P being Subset-Family of ultraset BL such that
A19: union P = p and
A20: P c= StoneR BL by A17;
consider Q being Subset-Family of ultraset BL such that
A21: union Q = q and
A22: Q c= StoneR BL by A18;
A23: union P /\ union Q = union INTERSECTION(P,Q) by SETFAM_1:28;
INTERSECTION(P,Q) c=bool ultraset BL
proof
let x be object;
assume x in INTERSECTION(P,Q);
then consider X,Y being set such that
A24: X in P and
A25: Y in Q and
A26: x = X /\ Y by SETFAM_1:def 5;
A27: X /\ Y c= X \/ Y by XBOOLE_1:29;
X \/ Y c= ultraset BL by A24,A25,XBOOLE_1:8;
then X /\ Y c= ultraset BL by A27;
hence thesis by A26;
end;
then reconsider C= INTERSECTION(P,Q) as Subset-Family of ultraset BL;
reconsider C as Subset-Family of ultraset BL;
C c= StoneR BL
proof
let x be object;
assume x in C;
then consider X,Y being set such that
A28: X in P and
A29: Y in Q and
A30: x = X /\ Y by SETFAM_1:def 5;
consider a such that
A31: X =(UFilter BL).a by A20,A28,Th23;
consider b such that
A32: Y =(UFilter BL).b by A22,A29,Th23;
A33: X={ F: F is being_ultrafilter & a in F} by A31,Def6;
A34: Y={ F: F is being_ultrafilter & b in F} by A32,Def6;
A35: X /\ Y = { F: F is being_ultrafilter & a "/\" b in F}
proof
A36: X /\ Y c= { F: F is being_ultrafilter & a "/\" b in F}
proof
let x be object;
assume
A37: x in X /\ Y;
then
A38: x in X by XBOOLE_0:def 4;
A39: x in Y by A37,XBOOLE_0:def 4;
consider F1 such that
A40: x= F1 and
A41: F1 is being_ultrafilter and
A42: a in F1 by A33,A38;
ex F2 st ( x= F2)&( F2 is being_ultrafilter)&( b in F2) by A34,A39;
then a "/\" b in F1 by A40,A42,FILTER_0:8;
hence thesis by A40,A41;
end;
{ F: F is being_ultrafilter & a "/\" b in F} c= X /\ Y
proof
let x be object;
assume x in { F: F is being_ultrafilter & a "/\" b in F};
then consider F0 such that
A43: x= F0 and
A44: F0 is being_ultrafilter and
A45: a "/\" b in F0;
a in F0 by A45,FILTER_0:8;
then consider F such that
A46: F=F0 and
A47: F is being_ultrafilter and
A48: a in F by A44;
A49: F in X by A33,A47,A48;
b in F0 by A45,FILTER_0:8;
then consider F1 such that
A50: F1=F0 and
A51: F1 is being_ultrafilter and
A52: b in F1 by A44;
F1 in Y by A34,A51,A52;
hence thesis by A43,A46,A49,A50,XBOOLE_0:def 4;
end;
hence thesis by A36;
end;
(UFilter BL).(a "/\" b)={ F :F is being_ultrafilter & (a "/\" b) in
F} by Def6;
hence thesis by A30,A35,Th23;
end;
hence thesis by A19,A21,A23;
end;
hence thesis by A1,A7,PRE_TOPC:def 1;
end;
then reconsider TS= TopStruct(# US,STP#) as strict TopSpace;
take TS;
thus thesis;
end;
uniqueness;
end;
registration
let BL;
cluster StoneSpace BL -> non empty;
coherence
proof
the carrier of StoneSpace BL =ultraset BL by Def8;
hence the carrier of StoneSpace BL is non empty;
end;
end;
theorem
F is being_ultrafilter & not F in UFilter BL.a implies not a in F by Th18;
theorem Th25:
ultraset BL \ UFilter BL.a = UFilter BL.a`
proof
hereby
let x be object;
assume
A1: x in ultraset BL \ UFilter BL.a;
then
A2: x in ultraset BL by XBOOLE_0:def 5;
A3: not x in UFilter BL.a by A1,XBOOLE_0:def 5;
consider F such that
A4: F=x and
A5: F is being_ultrafilter by A2;
not a in F by A3,A4,A5,Th18;
then a` in F by A5,FILTER_0:46;
hence x in UFilter BL.a` by A4,A5,Th18;
end;
let x be object;
assume x in UFilter BL.a`;
then consider F such that
A6: F=x and
A7: F is being_ultrafilter and
A8: a` in F by Th17;
A9: not a in F by A7,A8,FILTER_0:46;
A10: F in ultraset BL by A7;
not F in UFilter BL.a by A9,Th18;
hence x in ultraset BL \ UFilter BL.a by A6,A10,XBOOLE_0:def 5;
end;
definition
let BL;
func StoneBLattice BL -> Lattice equals
OpenClosedSetLatt(StoneSpace BL );
coherence;
end;
Lm1: for p being Subset of StoneSpace BL holds p in StoneR BL implies p is open
proof
let p be Subset of StoneSpace BL;
assume
A1: p in StoneR BL;
then
A2: {p} is Subset-Family of ultraset BL by SUBSET_1:41;
A3: {p} c= StoneR BL by A1,ZFMISC_1:31;
union {p} =p by ZFMISC_1:25;
then
p in {union A where A is Subset-Family of ultraset BL : A c= StoneR BL }
by A2,A3;
then p in the topology of StoneSpace BL by Def8;
hence thesis by PRE_TOPC:def 2;
end;
registration
let BL;
cluster UFilter BL -> one-to-one;
coherence
proof
now
let a,b;
assume that
A1: UFilter BL.a = UFilter BL.b;
assume not a=b;
then consider UF such that
A2: UF is being_ultrafilter and
A3: a in UF & not b in UF or not a in UF & b in UF by FILTER_0:47;
now per cases by A3;
case
A4: a in UF & not b in UF;
then UF in UFilter BL.a by A2,Th18;
hence UFilter BL.a <> UFilter BL.b by A4,Th18;
end;
case not a in UF & b in UF;
then not UF in UFilter BL.a by Th18;
hence UFilter BL.a <> UFilter BL.b by A2,A3,Th18;
end;
end;
hence contradiction by A1;
end;
hence thesis by GROUP_6:1;
end;
end;
theorem
union StoneR BL = ultraset BL
proof
set x = the Element of OpenClosedSet(StoneSpace BL);
reconsider X=x as Subset of StoneSpace BL;
A1: X is open by Th1;
A2: X is closed by Th2;
X in the topology of StoneSpace BL by A1,PRE_TOPC:def 2;
then X in {union A where A is Subset-Family of ultraset BL : A c= StoneR BL}
by Def8;
then consider B being Subset-Family of ultraset BL such that
A3: union B = X and
A4: B c= StoneR BL;
X` is open by A2;
then X` in the topology of StoneSpace BL by PRE_TOPC:def 2;
then X` in {union A where A is Subset-Family of ultraset BL :
A c= StoneR BL} by Def8;
then consider C being Subset-Family of ultraset BL such that
A5: union C = X` and
A6: C c= StoneR BL;
B \/ C c= StoneR BL by A4,A6,XBOOLE_1:8;
then union (B \/ C) c= union StoneR BL by ZFMISC_1:77;
then X \/ X` c= union StoneR BL by A3,A5,ZFMISC_1:78;
then [#] StoneSpace BL c= union StoneR BL by PRE_TOPC:2;
then
A7: ultraset BL c= union StoneR BL by Def8;
union StoneR BL c= union bool ultraset BL by ZFMISC_1:77;
then union StoneR BL c= ultraset BL by ZFMISC_1:81;
hence thesis by A7;
end;
theorem Th27:
for X being non empty set ex Y being Element of Fin X st Y is non empty
proof
let X be non empty set;
set a = the Element of X;
{. a .} is Element of Fin X;
hence thesis;
end;
registration
let D be non empty set;
cluster non empty for Element of Fin D;
existence by Th27;
end;
theorem Th28:
for L being non trivial B_Lattice, D being non empty Subset of L
st Bottom L in <.D.) ex B being non empty Element of Fin the carrier of L
st B c= D & FinMeet(B) = Bottom L
proof
let L be non trivial B_Lattice, D be non empty Subset of L such that
A1: Bottom L in <.D.);
set A = { FinMeet(C) where C is Element of Fin the carrier of L:
C c= D & C <> {} };
set AA = { a where a is Element of L:
ex c being Element of L st c in A & c [= a };
A2: AA c= the carrier of L
proof
let x be object;
assume x in AA;
then ex a being Element of L st ( a= x)&( ex c being Element of L
st c in A & c [= a);
hence thesis;
end;
AA is non empty
proof
consider C being Element of Fin D such that
A3: C is non empty by Th27;
A4: C is Subset of D by FINSUB_1:16;
then C c= the carrier of L by XBOOLE_1:1;
then C is Element of Fin the carrier of L by FINSUB_1:def 5;
then consider C being Element of Fin the carrier of L such that
A5: C <> {} and
A6: C c= D by A3,A4;
reconsider a = FinMeet(C) as Element of L;
a in A by A5,A6;
then a in AA;
hence thesis;
end;
then reconsider AA as non empty Subset of L by A2;
A7: for p,q being Element of L st p in AA & q in AA holds p "/\" q in AA
proof
let p,q be Element of L;
assume that
A8: p in AA and
A9: q in AA;
consider a being Element of L such that
A10: a= p and
A11: ex c being Element of L st c in A & c [= a by A8;
consider c being Element of L such that
A12: c in A and
A13: c [= a by A11;
consider b being Element of L such that
A14: b= q and
A15: ex d being Element of L st d in A & d [= b by A9;
consider d being Element of L such that
A16: d in A and
A17: d [= b by A15;
A18: c "/\" d [= a "/\" b by A13,A17,FILTER_0:5;
consider C being Element of Fin the carrier of L such that
A19: c = FinMeet(C) and
A20: C c= D and
A21: C <> {} by A12;
consider E being Element of Fin the carrier of L such that
A22: d = FinMeet(E) and
A23: E c= D and E <> {} by A16;
A24: c "/\" d = FinMeet(C \/ E) by A19,A22,LATTICE4:23;
C \/ E c= D by A20,A23,XBOOLE_1:8;
then c "/\" d in A by A21,A24;
hence thesis by A10,A14,A18;
end;
for p,q being Element of L st p in AA & p [= q holds q in AA
proof
let p,q be Element of L;
assume that
A25: p in AA and
A26: p [= q;
A27: ex a being Element of L st ( a= p)&( ex c being Element of L
st c in A & c [= a) by A25;
ex b being Element of L st ( b= q)&( ex c being Element of L
st c in A & c [= b) by A26,A27,LATTICES:7;
hence thesis;
end;
then
A28: AA is Filter of L by A7,FILTER_0:9;
D c= AA
proof
let x be object;
assume
A29: x in D;
then
A30: { x } c= D by ZFMISC_1:31;
{ x } c= the carrier of L by A29,ZFMISC_1:31;
then reconsider C = { x } as Element of Fin the carrier of L by FINSUB_1:def 5;
A31: x = (id the carrier of L).x by A29,FUNCT_1:18
.= (the L_meet of L)$$(C,id the carrier of L) by A29,SETWISEO:17
.= FinMeet(C,id L) by LATTICE2:def 4
.= FinMeet(C) by LATTICE4:def 9;
reconsider a = FinMeet(C) as Element of L;
a in A by A30;
hence thesis by A31;
end;
then <.D.) c= AA by A28,FILTER_0:def 4;
then Bottom L in AA by A1;
then ex d being Element of L st d = Bottom L &
ex c being Element of L st c in A & c [= d;
then consider c being Element of L such that
A32: c in A and
A33: c [= Bottom L;
Bottom L [= c;
then Bottom L in A by A32,A33,LATTICES:8;
then ex C being Element of Fin the carrier of L
st Bottom L = FinMeet(C) & C c= D & C <> {};
hence thesis;
end;
theorem Th29:
for L being 0_Lattice holds
not ex F being Filter of L st F is being_ultrafilter & Bottom L in F
proof
let L be 0_Lattice;
given F being Filter of L such that
A1: F is being_ultrafilter and
A2: Bottom L in F;
F = the carrier of L by A2,FILTER_0:26;
hence contradiction by A1,FILTER_0:def 3;
end;
theorem Th30:
UFilter BL.Bottom BL = {}
proof
assume
A1: UFilter BL.Bottom BL <> {};
set x = the Element of UFilter BL.Bottom BL;
ex F st F=x & F is being_ultrafilter & Bottom BL in F by A1,Th17;
hence contradiction by Th29;
end;
theorem
UFilter BL.Top BL = ultraset BL
proof
thus UFilter BL.Top BL = UFilter BL.(Bottom BL)` by LATTICE4:30
.= ultraset BL \ UFilter BL.Bottom BL by Th25
.= ultraset BL \ {} by Th30
.= ultraset BL;
end;
theorem Th32:
ultraset BL = union X & X is Subset of StoneR BL implies
ex Y being Element of Fin X st ultraset BL = union Y
proof
assume that
A1: ultraset BL = union X and
A2: X is Subset of StoneR BL;
assume
A3: not thesis;
consider Y being Element of Fin X such that
A4: Y is non empty by A1,Th27,ZFMISC_1:2;
A5: Y c= X by FINSUB_1:def 5;
then
A6: Y c= StoneR BL by A2,XBOOLE_1:1;
set x = the Element of Y;
A7: x in X by A4,A5;
x in StoneR BL by A4,A6;
then consider b such that
A8: x =UFilter BL.b by Th23;
set CY = { a` : UFilter BL.a in X };
consider c such that
A9: c = b`;
A10: c in CY by A7,A8,A9;
CY c= the carrier of BL
proof
let x be object;
assume x in CY;
then ex b st ( x = b`)&( UFilter BL.b in X);
hence thesis;
end;
then reconsider CY as non empty Subset of BL by A10;
set H = <.CY.);
for B being non empty Element of Fin the carrier of BL st B c= CY
holds FinMeet B <> Bottom BL
proof
let B be non empty Element of Fin the carrier of BL such that
A11: B c= CY and
A12: FinMeet B = Bottom BL;
A13: B is Subset of BL by FINSUB_1:16;
A14: dom UFilter BL = the carrier of BL by FUNCT_2:def 1;
UFilter BL.:B c= rng UFilter BL by RELAT_1:111;
then reconsider D = UFilter BL.:B
as non empty Subset-Family of ultraset BL by A13,A14,XBOOLE_1:1;
A15: now
set x = the Element of UFilter BL.Bottom BL;
assume {}ultraset BL <> UFilter BL.Bottom BL;
then ex F st F=x & F is being_ultrafilter & Bottom BL in F by Th17;
hence contradiction by Th29;
end;
deffunc U(Subset of ultraset BL,Subset of ultraset BL) = $1 /\ $2;
consider G being BinOp of bool ultraset BL such that
A16: for x,y being Subset of ultraset BL holds
G.(x,y)= U(x,y) from BINOP_1:sch 4;
A17: G is commutative
proof
let x,y be Subset of ultraset BL;
G. (x,y) = y /\ x by A16
.= G. (y,x) by A16;
hence thesis;
end;
A18: G is associative
proof
let x,y,z be Subset of ultraset BL;
G. (x,G. (y,z)) = G.(x, y /\ z) by A16
.= x /\ (y /\ z) by A16
.= (x /\ y) /\ z by XBOOLE_1:16
.= G.(x /\ y, z) by A16
.= G. (G.(x,y),z) by A16;
hence thesis;
end;
A19: G is idempotent
proof
let x be Subset of ultraset BL;
G. (x,x) = x /\ x by A16
.= x;
hence thesis;
end;
A20: for x,y being Element of BL holds
UFilter BL.((the L_meet of BL).(x,y)) = G.(UFilter BL.x,UFilter BL.y)
proof
let x,y be Element of BL;
thus UFilter BL.((the L_meet of BL).(x,y)) = UFilter BL.(x "/\" y)
.=UFilter BL.x /\ UFilter BL.y by Th20
.=G.(UFilter BL.x,UFilter BL.y) by A16;
end;
reconsider DD = D as Element of Fin bool ultraset BL;
id BL = id the carrier of BL;
then
A21: UFilter BL.FinMeet B
= UFilter BL.(FinMeet(B,id the carrier of BL)) by LATTICE4:def 9
.= UFilter BL.((the L_meet of BL)$$(B,id the carrier of BL))
by LATTICE2:def 4
.= G$$(B,(UFilter BL)*(id the carrier of BL))
by A17,A18,A19,A20,SETWISEO:30
.= G$$(B,UFilter BL) by FUNCT_2:17
.= G$$(B,(id bool ultraset BL)*UFilter BL) by FUNCT_2:17
.= G$$(DD,id bool ultraset BL) by A17,A18,A19,SETWISEO:29;
defpred X[Element of Fin bool ultraset BL] means
for D being non empty Subset-Family of ultraset BL st
D = $1 holds G$$($1,id bool ultraset BL) = meet D;
A22: X[{}.bool ultraset BL];
A23: for DD being (Element of Fin bool ultraset BL),
b being Subset of ultraset BL st X[DD] holds X[DD \/ {.b.}]
proof
let DD be (Element of Fin bool ultraset BL), b be Subset of ultraset BL;
assume
A24: for D being non empty Subset-Family of ultraset BL st D = DD
holds G$$(DD,id bool ultraset BL) = meet D;
let D be non empty Subset-Family of ultraset BL such that
A25: D = DD \/ {b};
now per cases;
suppose
A26: DD is empty;
hence G$$(DD \/ {.b.},id bool ultraset BL)=
(id bool ultraset BL).b by A17,A18,SETWISEO:17
.= b
.= meet D by A25,A26,SETFAM_1:10;
end;
suppose
A27: DD is non empty;
DD c= D by A25,XBOOLE_1:7;
then reconsider D1=DD as non empty Subset-Family of ultraset BL
by A27,XBOOLE_1:1;
reconsider D1 as non empty Subset-Family of ultraset BL;
thus G$$(DD \/ {.b.},id bool ultraset BL) =
G.(G$$(DD,id bool ultraset BL),(id bool ultraset BL).b)
by A17,A18,A19,A27,SETWISEO:20
.= G.(G$$(DD,id bool ultraset BL), b)
.= G$$(DD,id bool ultraset BL) /\ b by A16
.= meet D1 /\ b by A24
.= meet D1 /\ meet {b} by SETFAM_1:10
.= meet D by A25,SETFAM_1:9;
end;
end;
hence thesis;
end;
for DD being Element of Fin bool ultraset BL holds X[DD]
from SETWISEO:sch 4(A22,A23);
then meet D = {}ultraset BL by A12,A15,A21;
then
A28: union COMPLEMENT D = [#] ultraset BL \ {} by SETFAM_1:34
.= ultraset BL;
A29: COMPLEMENT D c= X
proof
let x be object;
assume
A30: x in COMPLEMENT D;
then reconsider c = x as Subset of ultraset BL;
c` in D by A30,SETFAM_1:def 7;
then consider a being object such that
A31: a in dom UFilter BL and
A32: a in B and
A33: c` = UFilter BL.a by FUNCT_1:def 6;
reconsider a as Element of BL by A31;
a in CY by A11,A32;
then a`` in CY;
then consider b being Element of BL such that
A34: b` = a`` and
A35: UFilter BL.b in X;
x = (UFilter BL.a)` by A33
.= UFilter BL.a` by Th25
.= UFilter BL.b`` by A34
.= UFilter BL.b;
hence thesis by A35;
end;
COMPLEMENT D is finite
proof
A36: D is finite;
deffunc U(Subset of ultraset BL) = $1`;
A37: { U(w) where w is Subset of ultraset BL : w in D } is finite
from FRAENKEL:sch 21(A36);
{ w` where w is Subset of ultraset BL: w in D } = COMPLEMENT(D)
proof
hereby
let x be object;
assume x in { w` where w is Subset of ultraset BL : w in D };
then consider w being Subset of ultraset BL such that
A38: w` = x and
A39: w in D;
w`` in D by A39;
hence x in COMPLEMENT(D) by A38,SETFAM_1:def 7;
end;
let x be object;
assume
A40: x in COMPLEMENT(D);
then reconsider x9 = x as Subset of ultraset BL;
A41: x9` in D by A40,SETFAM_1:def 7;
x9``= x9;
hence thesis by A41;
end;
hence thesis by A37;
end;
then COMPLEMENT D is Element of Fin X by A29,FINSUB_1:def 5;
hence contradiction by A3,A28;
end;
then H <> the carrier of BL by Th28;
then consider F such that
A42: H c= F and
A43: F is being_ultrafilter by FILTER_0:18;
A44: CY c= H by FILTER_0:def 4;
not F in union X
proof
assume F in union X;
then consider Y being set such that
A45: F in Y and
A46: Y in X by TARSKI:def 4;
consider a being object such that
A47: a in dom UFilter BL and
A48: Y = UFilter BL.a by A2,A46,FUNCT_1:def 3;
reconsider a as Element of BL by A47;
a` in CY by A46,A48;
then
A49: a` in H by A44;
a in F by A45,A48,Th18;
hence contradiction by A42,A43,A49,FILTER_0:46;
end;
hence contradiction by A1,A43;
end;
Lm2: StoneR BL c= OpenClosedSet(StoneSpace BL)
proof
let x be object;
assume
A1: x in StoneR BL;
then reconsider p = x as Subset of StoneSpace BL by Def8;
A2: p is open by A1,Lm1;
p is closed
proof
set ST=StoneSpace BL;
A3: [#] ST = ultraset BL by Def8;
consider a such that
A4: UFilter BL.a=p by A1,Th23;
p` = UFilter BL.a` by A3,A4,Th25;
then p` in StoneR BL by Th23;
then p` is open by Lm1;
hence thesis by TOPS_1:3;
end;
hence thesis by A2;
end;
theorem Th33:
StoneR BL = OpenClosedSet(StoneSpace BL)
proof
A1: StoneR BL c= OpenClosedSet(StoneSpace BL) by Lm2;
OpenClosedSet(StoneSpace BL) c= StoneR BL
proof
let x be object;
assume
A2: x in OpenClosedSet(StoneSpace BL);
then reconsider X=x as Subset of StoneSpace BL;
A3: the topology of StoneSpace BL =
{union A where A is Subset-Family of ultraset BL : A c= StoneR BL }
by Def8;
A4: X is open closed by A2,Th1,Th2;
then
A5: X` is open closed;
X in the topology of StoneSpace BL by A4,PRE_TOPC:def 2;
then consider A1 being Subset-Family of ultraset BL such that
A6: X = union A1 and
A7: A1 c= StoneR BL by A3;
X` in the topology of StoneSpace BL by A5,PRE_TOPC:def 2;
then consider A2 being Subset-Family of ultraset BL such that
A8: X` = union A2 and
A9: A2 c= StoneR BL by A3;
A10: X is Subset of ultraset BL by Def8;
set AA = A1 \/ A2;
A11: ultraset BL = [#] StoneSpace BL by Def8
.= X \/ X` by PRE_TOPC:2
.= union AA by A6,A8,ZFMISC_1:78;
A12: AA c= StoneR BL by A7,A9,XBOOLE_1:8;
then consider Y being Element of Fin AA such that
A13: ultraset BL = union Y by A11,Th32;
A14: Y c= AA by FINSUB_1:def 5;
then
A15: Y c= StoneR BL by A12;
set D = A1 /\ Y;
A16: Y = AA /\ Y by A14,XBOOLE_1:28
.= D \/ A2 /\ Y by XBOOLE_1:23;
now
let y be set;
assume y in A2 /\ Y;
then y in A2 by XBOOLE_0:def 4;
then
A17: y c= X` by A8,ZFMISC_1:74;
( X`) misses X by XBOOLE_1:79;
then ( X`) /\ X = {};
then y /\ X = {} by A17,XBOOLE_1:3,26;
hence y misses X;
end;
then
A18: X c= union D by A10,A13,A16,SETFAM_1:42;
per cases;
suppose D = {};
then
A19: X = {} by A18,ZFMISC_1:2;
{}=UFilter BL.Bottom BL by Th30;
hence thesis by A19,FUNCT_2:4;
end;
suppose
A20: D <> {};
A21: D c= Y by XBOOLE_1:17;
reconsider D as non empty Subset-Family of ultraset BL by A20;
reconsider D as non empty Subset-Family of ultraset BL;
A22: union D c= union A1 /\ union Y by ZFMISC_1:79;
union A1 /\ union Y c= union A1 by XBOOLE_1:17;
then union D c= X by A6,A22;
then
A23: X = union D by A18;
A24: D c= rng UFilter BL by A15,A21;
A25: rng UFilter BL = dom id StoneR BL;
A26: dom UFilter BL = dom UFilter BL;
UFilter BL = id StoneR BL*UFilter BL by RELAT_1:54;
then
UFilter BL, id StoneR BL are_fiberwise_equipotent by A25,A26,CLASSES1:77;
then card(UFilter BL"D) = card((id StoneR BL)"D) by CLASSES1:78
.= card D by A24,FUNCT_2:94;
then UFilter BL"D is finite;
then reconsider B = UFilter BL"D as
Element of Fin the carrier of BL by FINSUB_1:def 5;
A27: D = UFilter BL.:B by A15,A21,FUNCT_1:77,XBOOLE_1:1;
then
A28: B is non empty;
deffunc U(Subset of ultraset BL,Subset of ultraset BL) = $1 \/ $2;
consider G being BinOp of bool ultraset BL such that
A29: for x,y being Subset of ultraset BL holds
G.(x,y)= U(x,y) from BINOP_1:sch 4;
A30: G is commutative
proof
let x,y be Subset of ultraset BL;
G. (x,y) =y \/ x by A29
.= G. (y,x) by A29;
hence thesis;
end;
A31: G is associative
proof
let x,y,z be Subset of ultraset BL;
G. (x,G. (y,z)) = G.(x, y \/ z) by A29
.= x \/ (y \/ z) by A29
.= (x \/ y) \/ z by XBOOLE_1:4
.= G.(x \/ y, z) by A29
.= G. (G.(x,y),z) by A29;
hence thesis;
end;
A32: G is idempotent
proof
let x be Subset of ultraset BL;
G. (x,x) = x \/ x by A29
.= x;
hence thesis;
end;
A33: for x,y being Element of BL holds
UFilter BL.((the L_join of BL).(x,y)) = G.(UFilter BL.x,UFilter BL.y)
proof
let x,y be Element of BL;
thus
UFilter BL.((the L_join of BL).(x,y)) = UFilter BL.(x "\/" y)
.=UFilter BL.x \/ UFilter BL.y by Th21
.=G.(UFilter BL.x,UFilter BL.y) by A29;
end;
reconsider DD = D as Element of Fin bool ultraset BL by FINSUB_1:def 5;
id BL = id the carrier of BL;
then
A34: UFilter BL.FinJoin B
= UFilter BL.(FinJoin(B,id the carrier of BL)) by LATTICE4:def 8
.= UFilter BL.((the L_join of BL)$$(B,id the carrier of BL))
by LATTICE2:def 3
.= G$$(B,(UFilter BL)*(id the carrier of BL))
by A28,A30,A31,A32,A33,SETWISEO:30
.= G$$(B,UFilter BL) by FUNCT_2:17
.= G$$(B,(id bool ultraset BL)*UFilter BL) by FUNCT_2:17
.= G$$(DD,id bool ultraset BL) by A27,A28,A30,A31,A32,SETWISEO:29;
defpred X[Element of Fin bool ultraset BL] means
for D being non empty Subset-Family of ultraset BL st
D = $1 holds G$$($1,id bool ultraset BL) = union D;
A35: X[{}.bool ultraset BL];
A36: for DD being (Element of Fin bool ultraset BL),
b being Subset of ultraset BL st X[DD] holds X[DD \/ {.b.}]
proof
let DD be (Element of Fin bool ultraset BL),
b be Subset of ultraset BL;
assume
A37: for D being non empty Subset-Family of ultraset BL st D = DD
holds G$$(DD,id bool ultraset BL) = union D;
let D be non empty Subset-Family of ultraset BL such that
A38: D = DD \/ {b};
now per cases;
suppose
A39: DD is empty;
hence G$$(DD \/ {.b.},id bool ultraset BL)=
(id bool ultraset BL).b by A30,A31,SETWISEO:17
.= b
.= union D by A38,A39,ZFMISC_1:25;
end;
suppose
A40: DD is non empty;
DD c= D by A38,XBOOLE_1:7;
then reconsider D1=DD as non empty Subset-Family of ultraset BL
by A40,XBOOLE_1:1;
reconsider D1 as non empty Subset-Family of ultraset BL;
thus G$$(DD \/ {.b.},id bool ultraset BL) =
G.(G$$(DD,id bool ultraset BL),(id bool ultraset BL).b)
by A30,A31,A32,A40,SETWISEO:20
.= G.(G$$(DD,id bool ultraset BL), b)
.= G$$(DD,id bool ultraset BL) \/ b by A29
.= union D1 \/ b by A37
.= union D1 \/ union {b} by ZFMISC_1:25
.= union D by A38,ZFMISC_1:78;
end;
end;
hence thesis;
end;
for DD being Element of Fin bool ultraset BL holds X[DD]
from SETWISEO:sch 4(A35,A36);
then UFilter BL.FinJoin B = x by A23,A34;
hence thesis by FUNCT_2:4;
end;
end;
hence thesis by A1;
end;
definition
let BL;
redefine func UFilter BL -> Homomorphism of BL,StoneBLattice BL; :: redefines UFilter (LOPCLSET, definition)
coherence
proof
reconsider g=UFilter BL as Function of the carrier of BL,
bool ultraset BL;
set SL=StoneBLattice BL;
rng g = StoneR BL;
then rng g c= OpenClosedSet(StoneSpace BL) by Lm2;
then reconsider f=UFilter BL as Function of the carrier of BL,
the carrier of SL by FUNCT_2:6;
now
let p,q;
thus f.(p "\/" q) = f.p \/ f.q by Th21
.= f.p "\/" f.q by Def2;
thus f.(p "/\" q) = f.p /\ f.q by Th20
.= f.p "/\" f.q by Def3;
end;
then f is "\/"-preserving "/\"-preserving by LATTICE4:def 1,def 2;
hence thesis;
end;
end;
theorem Th34:
rng UFilter BL = the carrier of StoneBLattice BL
proof
thus rng UFilter BL= StoneR BL .= the carrier of StoneBLattice BL by Th33;
end;
registration
let BL;
cluster UFilter BL -> bijective for Function of BL,StoneBLattice BL;
coherence
proof
rng UFilter BL = the carrier of StoneBLattice BL by Th34;
then UFilter BL is onto by FUNCT_2:def 3;
hence thesis;
end;
end;
theorem Th35:
BL,StoneBLattice BL are_isomorphic
proof
ex f being Homomorphism of BL,StoneBLattice BL st
f=UFilter BL & f is bijective;
hence thesis by LATTICE4:def 3;
end;
::$N Stone Representation Theorem for Boolean Algebras
theorem
for BL being non trivial B_Lattice ex T being non empty TopSpace st
BL, OpenClosedSetLatt(T) are_isomorphic
proof
let BL be non trivial B_Lattice;
reconsider T = StoneSpace BL as non empty TopSpace;
take T;
OpenClosedSetLatt(T) = StoneBLattice BL;
hence thesis by Th35;
end;