Copyright (c) 1993 Association of Mizar Users
environ
vocabulary LATTICE2, FILTER_0, LATTICES, PRE_TOPC, BOOLE, TOPS_1, SUBSET_1,
SETFAM_1, BINOP_1, FUNCT_1, RELAT_1, ZFMISC_1, TARSKI, GROUP_6, MOD_4,
WELLORD1, REALSET1, ZF_LANG, LATTICE4, OPENLATT, HAHNBAN;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, RELAT_1, FUNCT_1,
FUNCT_2, BINOP_1, SETFAM_1, STRUCT_0, PRE_TOPC, TOPS_1, LATTICES,
LATTICE2, FILTER_0, REALSET1, LATTICE4;
constructors BINOP_1, TOPS_1, LATTICE2, REALSET1, FILTER_1, LATTICE4;
clusters FILTER_0, PRE_TOPC, LATTICE2, RLSUB_2, STRUCT_0, RELSET_1, SUBSET_1,
LATTICES, XBOOLE_0, ZFMISC_1;
requirements BOOLE, SUBSET;
definitions TARSKI, PRE_TOPC, FILTER_0, LATTICES, LATTICE4, FUNCT_1, REALSET1,
STRUCT_0, XBOOLE_0;
theorems PRE_TOPC, LATTICES, TOPS_1, ZFMISC_1, FILTER_0, SETFAM_1, TARSKI,
FUNCT_1, FUNCT_2, LATTICE2, BORSUK_1, LATTICE4, REALSET1, RELAT_1,
ORDINAL1, XBOOLE_0, XBOOLE_1;
schemes BINOP_1, DOMAIN_1, FUNCT_1, COMPLSP1;
begin
definition
cluster Heyting -> implicative 0_Lattice;
coherence by LATTICE2:def 6;
cluster implicative -> upper-bounded Lattice;
coherence by FILTER_0:37;
end;
reserve T for TopSpace;
reserve A,B for Subset of T;
theorem
Th1: A /\ Int(A` \/ B) c= B
proof
Int(A` \/ B) c= A` \/ B by TOPS_1:44;
then A1: A /\ Int(A` \/ B) c= A /\ (A` \/ B) by XBOOLE_1:26;
A2: A misses A` by PRE_TOPC:26;
A /\ (A` \/ B) = (A /\ A`) \/ A /\ B by XBOOLE_1:23
.= {} \/ A /\ B by A2,XBOOLE_0:def 7
.= A /\ B;
then A /\ (A` \/ B)c= B by XBOOLE_1:17;
hence thesis by A1,XBOOLE_1:1;
end;
theorem Th2:
for C being Subset of T st C is open & A /\ C c= B holds C c= Int(A` \/ B)
proof
let C be Subset of T;
assume A1: C is open & A /\ C c= B;
A2: C c= C \/ A` by XBOOLE_1:7;
(A /\ C) \/ A` = (A \/ A`) /\ (C \/ A`) by XBOOLE_1:24
.= [#] T /\ (C \/ A`) by PRE_TOPC:18
.= C \/ A` by PRE_TOPC:15;
then C \/ A` c= B \/ A` by A1,XBOOLE_1:9;
then C c= B \/ A` by A2,XBOOLE_1:1;
then Int(C) c= Int(A` \/ B) by TOPS_1:48;
hence thesis by A1,TOPS_1:55;
end;
definition let T be TopStruct;
func Topology_of T -> Subset-Family of T equals
:Def1: the topology of T;
coherence;
end;
definition let T;
cluster Topology_of T -> non empty;
coherence
proof
Topology_of T = the topology of T by Def1;
hence thesis by PRE_TOPC:5;
end;
end;
theorem Th3:
for A being Subset of T holds A is open iff A in Topology_of T
proof
let A be Subset of T;
A is open iff A in the topology of T by PRE_TOPC:def 5;
hence thesis by Def1;
end;
definition let T be non empty TopSpace,
P, Q be Element of Topology_of T;
redefine func P \/ Q -> Element of Topology_of T;
coherence
proof
reconsider A = P, B = Q as Subset of T;
A is open & B is open by Th3;
then P \/ Q is open by TOPS_1:37;
hence thesis by Th3;
end;
redefine func P /\ Q -> Element of Topology_of T;
coherence
proof
reconsider A = P, B = Q as Subset of T;
A is open & B is open by Th3;
then P /\ Q is open by TOPS_1:38;
hence thesis by Th3;
end;
end;
reserve T for non empty TopSpace;
reserve P,Q for Element of Topology_of T;
definition let T;
func Top_Union T -> BinOp of Topology_of T means
:Def2: it.(P,Q) = P \/ Q;
existence
proof
deffunc F(Element of Topology_of T, Element of Topology_of T) = $1 \/ $2;
thus ex F being BinOp of Topology_of T st
for P,Q being Element of Topology_of T holds
F.(P,Q) = F(P,Q) from BinOpLambda;
end;
uniqueness
proof
set A = Topology_of T;
deffunc O(Element of A, Element of A) = $1 \/ $2;
thus for o1,o2 being BinOp of A st
(for a,b being Element of A holds o1.(a,b) = O(a,b)) &
(for a,b being Element of A holds o2.(a,b) = O(a,b))
holds o1 = o2 from BinOpDefuniq;
end;
func Top_Meet T -> BinOp of Topology_of T means
:Def3: it.(P,Q) = P /\ Q;
existence
proof
deffunc F(Element of Topology_of T, Element of Topology_of T) = $1 /\ $2;
thus ex F being BinOp of Topology_of T st
for P,Q being Element of Topology_of T holds
F.(P,Q) = F(P,Q) from BinOpLambda;
end;
uniqueness
proof
set A = Topology_of T;
deffunc O(Element of A, Element of A) = $1 /\ $2;
thus for o1,o2 being BinOp of A st
(for a,b being Element of A holds o1.(a,b) = O(a,b)) &
(for a,b being Element of A holds o2.(a,b) = O(a,b))
holds o1 = o2 from BinOpDefuniq;
end;
end;
Lm1: for p,q be Element of
LattStr(#Topology_of T,Top_Union T,Top_Meet T#)
holds p"\/"q = p \/ q
proof
let p,q be Element of
LattStr(#Topology_of T,Top_Union T,Top_Meet T#);
thus p"\/"q =(Top_Union T).(p,q) by LATTICES:def 1
.= p \/ q by Def2;
end;
Lm2: for p,q be Element of
LattStr(#Topology_of T,Top_Union T,Top_Meet T#)
holds p "/\" q = p /\ q
proof
let p,q be Element of
LattStr(#Topology_of T,Top_Union T,Top_Meet T#);
thus p"/\"q =(Top_Meet T).(p,q) by LATTICES:def 2
.= p /\ q by Def3;
end;
theorem
Th4: for T being non empty TopSpace holds
LattStr(#Topology_of T,Top_Union T,Top_Meet T#) is Lattice
proof let T;
set L = LattStr(#Topology_of T,Top_Union T,Top_Meet T#);
A1: now let p,q be Element of L;
thus p "\/" q = q \/ p by Lm1
.= q"\/"p by Lm1;
end;
A2: now let p,q,r be Element of L;
thus p"\/"(q"\/"r) = p \/ q "\/" r by Lm1
.= p \/ (q \/ r) by Lm1
.= (p \/ q) \/ r by XBOOLE_1:4
.= p "\/" q \/ r by Lm1
.= (p"\/"q)"\/"r by Lm1;
end;
A3: now let p,q be Element of L;
thus (p"/\"q)"\/"q = p"/\"q \/ q by Lm1
.= (p /\ q) \/ q by Lm2
.= q by XBOOLE_1:22;
end;
A4: now let p,q be Element of L;
thus p "/\" q =q /\ p by Lm2
.= q"/\"p by Lm2;
end;
A5: now let p,q,r be Element of L;
thus p"/\"(q"/\"r) = p /\ (q "/\" r) by Lm2
.= p /\ (q /\ r) by Lm2
.= (p /\ q) /\ r by XBOOLE_1:16
.= p "/\" q /\ r by Lm2
.= (p"/\"q)"/\"r by Lm2;
end;
now let p,q be Element of L;
thus p"/\"(p"\/"q) = p /\ (p"\/"q) by Lm2
.= p /\ (p \/ q) by Lm1
.= p by XBOOLE_1:21;
end;
then L is join-commutative join-associative meet-absorbing
meet-commutative meet-associative join-absorbing by A1,A2,A3,A4,A5,
LATTICES:def 4,def 5,def 6,def 7,def 8,def 9;
hence L is Lattice by LATTICES:def 10;
end;
definition let T;
func Open_setLatt(T) -> Lattice equals
:Def4: LattStr(#Topology_of T,Top_Union T,Top_Meet T#);
coherence by Th4;
end;
theorem
Th5: the carrier of Open_setLatt(T) = Topology_of T
proof
Open_setLatt(T) = LattStr(#Topology_of T,Top_Union T,Top_Meet T#) by Def4
;
hence thesis;
end;
reserve p,q for Element of Open_setLatt(T);
theorem
Th6: p "\/" q = p \/ q & p "/\" q = p /\ q
proof
A1: Open_setLatt(T) =LattStr(#Topology_of T,Top_Union T,Top_Meet T#)
by Def4;
then reconsider p' = p,q' = q as Element of Topology_of T;
thus p "\/" q =(Top_Union T).(p',q') by A1,LATTICES:def 1
.=p \/ q by Def2;
thus p "/\" q =(Top_Meet T).(p',q') by A1,LATTICES:def 2
.=p /\ q by Def3;
end;
theorem
Th7: p [= q iff p c= q
proof
(p [= q iff p "\/" q = q) & p "\/" q = p \/ q by Th6,LATTICES:def 3;
hence thesis by XBOOLE_1:7,12;
end;
theorem
Th8: for p',q' being Element of Topology_of T st p=p' & q=q'
holds p [= q iff p' c= q'
proof
let p',q' be Element of Topology_of T such that
A1: p=p' & q=q';
A2: Open_setLatt(T) = LattStr(#Topology_of T,Top_Union T,Top_Meet T#)
by Def4;
hereby assume A3: p [= q;
p' \/ q' = (Top_Union T).(p',q') by Def2
.= p"\/"q by A1,A2,LATTICES:def 1
.= q' by A1,A3,LATTICES:def 3;
hence p' c= q' by XBOOLE_1:7;
end;
assume A4:p' c= q';
p "\/" q = (Top_Union T).(p,q) by A2,LATTICES:def 1
.= p' \/ q' by A1,Def2
.=q by A1,A4,XBOOLE_1:12;
hence p [= q by LATTICES:def 3;
end;
theorem
Th9: Open_setLatt(T) is implicative
proof
set OL=Open_setLatt(T);
A1: OL= LattStr(#Topology_of T,Top_Union T,Top_Meet T#) by Def4;
let p,q be Element of OL;
reconsider p'=p, q'=q as Element of Topology_of T by A1;
Int(p'` \/ q') is open by TOPS_1:51;
then reconsider r'= Int(p'` \/ q') as Element of Topology_of T by Th3;
reconsider r=r' as Element of OL by A1;
take r;
A2: p' /\ r c= q' by Th1;
p "/\" r = p' /\ r' by Th6;
hence p "/\" r [= q by A2,Th8;
let r1 be Element of OL;
reconsider r2 = r1 as Element of Topology_of T by A1;
reconsider r1'= r2 as Subset of T;
A3: r1' is open by Th3;
assume A4: p "/\" r1 [= q;
p "/\" r1 = p' /\ r1' by A1,Lm2;
then p' /\ r2 c= q' by A4,Th8;
then r1' c= r' by A3,Th2;
hence r1 [= r by Th8;
end;
theorem
Th10: Open_setLatt(T) is lower-bounded & Bottom Open_setLatt(T) = {}
proof
set OL=Open_setLatt(T);
{} in the topology of T by PRE_TOPC:5;
then {} in Topology_of T by Def1;
then reconsider r = {} as Element of OL by Th5;
A1: now let p;
thus r"/\"p = r /\ p by Th6
.= r;
hence p"/\"r=r;
end;
thus OL is lower-bounded
proof
take r;
thus thesis by A1;
end;
hence thesis by A1,LATTICES:def 16;
end;
definition let T;
cluster Open_setLatt(T) -> Heyting;
coherence
proof
reconsider OL=Open_setLatt(T) as 0_Lattice by Th10;
OL is I_Lattice by Th9;
hence thesis by LATTICE2:def 6;
end;
end;
theorem
Th11: Top Open_setLatt(T) = the carrier of T
proof
set OL=Open_setLatt(T);
A1: OL= LattStr(#Topology_of T,Top_Union T,Top_Meet T#) by Def4;
the carrier of T in the topology of T by PRE_TOPC:def 1;
then reconsider B = the carrier of T
as Element of OL by A1,Def1;
now let p be Element of OL;
reconsider p'=p as Element of Topology_of T by A1;
thus B"\/"p = (the carrier of T) \/ p' by Th6
.= B by XBOOLE_1:12;
hence p"\/"B = B;
end;
hence thesis by LATTICES:def 17;
end;
reserve L for D_Lattice;
reserve F for Filter of L;
reserve a,b for Element of L;
reserve x,X,X1,X2,Y,Z for set;
definition let L;
func F_primeSet(L) -> set equals
:Def5: { F: F <> the carrier of L & F is prime};
coherence;
end;
theorem
Th12: F in F_primeSet(L) iff F <> the carrier of L & F is prime
proof
F_primeSet(L) = { F0 where F0 is Filter of L:
F0 <> the carrier of L & F0 is prime} by Def5;
then F in F_primeSet(L) iff
ex F0 being Filter of L st F0=F & F0 <> the carrier of L & F0 is prime;
hence thesis;
end;
definition let L;
func StoneH(L) -> Function means
:Def6: dom it = the carrier of L &
it.a = { F :F in F_primeSet(L) & a in F};
existence
proof
deffunc F(set) = { F :F in F_primeSet(L) & $1 in F};
consider f being Function such that
A1: dom f = the carrier of L & for x st x in the carrier of L
holds f.x = F(x) from Lambda;
take f;
thus thesis by A1;
end;
uniqueness
proof
let f1,f2 be Function;
assume that
A2: dom f1 = the carrier of L & f1.a={ F :F in F_primeSet(L) & a in F} and
A3: dom f2 = the carrier of L & f2.a={ F :F in F_primeSet(L) & a in F};
now let x;
assume x in the carrier of L;
then reconsider a=x as Element of L;
thus f1.x = { F :F in F_primeSet(L) & a in F} by A2
.= f2.x by A3;
end;
hence f1 = f2 by A2,A3,FUNCT_1:9;
end;
end;
theorem
Th13: F in StoneH(L).a iff F in F_primeSet(L) & a in F
proof
StoneH(L).a = {F0 where F0 is Filter of L: F0 in F_primeSet(L) & a in F0}
by Def6;
then F in StoneH(L).a iff
(ex F0 being Filter of L st F=F0 & F0 in F_primeSet(L) & a in F0);
hence thesis;
end;
theorem
Th14: x in StoneH(L).a iff
(ex F st F=x & F <> the carrier of L & F is prime & a in F)
proof
A1: StoneH(L).a = {F: F in F_primeSet(L) & a in F} by Def6;
hereby assume x in StoneH(L).a;
then consider F such that
A2: x=F & F in F_primeSet(L) & a in F by A1;
F <> the carrier of L & F is prime by A2,Th12;
hence ex F st F=x & F <> the carrier of L & F is prime & a in F by A2;
end;
given F such that
A3: F=x & F <> the carrier of L & F is prime & a in F;
F in F_primeSet(L) by A3,Th12;
hence x in StoneH(L).a by A1,A3;
end;
definition let L;
func StoneS(L) -> set equals
:Def7: rng StoneH(L);
coherence;
end;
definition let L;
cluster StoneS(L) -> non empty;
coherence
proof
A1: StoneS(L) = rng StoneH(L) by Def7;
dom StoneH(L) = the carrier of L by Def6;
hence thesis by A1,RELAT_1:65;
end;
end;
theorem
Th15: x in StoneS(L) iff ex a st x=StoneH(L).a
proof
hereby
assume x in StoneS(L);
then x in rng StoneH(L) by Def7;
then consider y be set such that
A1: y in dom StoneH(L) & x = StoneH(L).y by FUNCT_1:def 5;
reconsider y as Element of L by A1,Def6;
take y;
thus x=StoneH(L).y by A1;
end;
given b such that
A2: x=StoneH(L).b;
b in the carrier of L;
then b in dom StoneH(L) by Def6;
then x in rng StoneH(L) by A2,FUNCT_1:def 5;
hence x in StoneS(L) by Def7;
end;
theorem
Th16: StoneH(L).(a "\/" b) = StoneH(L).a \/ StoneH(L).b
proof
hereby let x;
set c = a "\/" b;
assume x in StoneH(L).c;
then consider F such that
A1: x=F & F <> the carrier of L & F is prime & c in F by Th14;
a in F or b in F by A1,FILTER_0:def 6;
then F in StoneH(L).a or F in StoneH(L).b by A1,Th14;
hence x in StoneH(L).a \/ StoneH(L).b by A1,XBOOLE_0:def 2;
end;
let x;
set c = a "\/" b;
assume x in StoneH(L).a \/ StoneH(L).b;
then x in StoneH(L).a or x in StoneH(L).b by XBOOLE_0:def 2;
then (ex F st x=F & F <> the carrier of L & F is prime & a in F )
or (ex F st x=F & F <> the carrier of L & F is prime & b in F) by Th14;
then consider F such that
A2: x=F & F <> the carrier of L & F is prime & (a in F or b in F);
c in F by A2,FILTER_0:def 6;
hence x in StoneH(L).c by A2,Th14;
end;
theorem
Th17: StoneH(L).(a "/\" b) = StoneH(L).a /\ StoneH(L).b
proof
hereby let x;
set c = a "/\" b;
assume x in StoneH(L).c;
then consider F such that
A1: x=F & F <> the carrier of L & F is prime & c in F by Th14;
a in F & b in F by A1,FILTER_0:def 1;
then F in StoneH(L).a & F in StoneH(L).b by A1,Th14;
hence x in StoneH(L).a /\ StoneH(L).b by A1,XBOOLE_0:def 3;
end;
let x;
set c = a "/\" b;
assume x in StoneH(L).a /\ StoneH(L).b;
then x in StoneH(L).a & x in StoneH(L).b by XBOOLE_0:def 3;
then ( ex F st x=F & F <> the carrier of L & F is prime & a in F )
& ( ex F st x=F & F <> the carrier of L & F is prime & b in F ) by Th14;
then consider F such that
A2: x=F & F <> the carrier of L & F is prime & (a in F & b in F);
c in F by A2,FILTER_0:def 1;
hence x in StoneH(L).c by A2,Th14;
end;
definition let L, a;
func SF_have a -> Subset-Family of L equals
:Def8: { F : a in F };
coherence
proof
set A= { F : a in F};
A c= bool the carrier of L
proof
let x;
assume x in A;
then ex F st x=F & a in F;
hence x in bool the carrier of L;
end;
then A is Subset-Family of L by SETFAM_1:def 7;
hence thesis;
end;
end;
definition
let L;let a;
cluster SF_have a -> non empty;
coherence
proof
a in <.a.) by FILTER_0:19;
then <.a.) in { F : a in F};
hence thesis by Def8;
end;
end;
theorem
Th18: x in SF_have a iff x is Filter of L & a in x
proof
SF_have a = { F: a in F } by Def8;
then x in SF_have a iff ex F st F=x & a in F;
hence thesis;
end;
Lm3: F in SF_have b \ SF_have a iff b in F & not a in F
proof
F in SF_have b \ SF_have a iff F in SF_have b & not F in SF_have a
by XBOOLE_0:def 4;
hence thesis by Th18;
end;
theorem
Th19: x in SF_have b \ SF_have a implies
x is Filter of L & b in x & not a in x
proof
assume x in SF_have b \ SF_have a;
then x in SF_have b & not x in SF_have a by XBOOLE_0:def 4;
then x is Filter of L & b in x & (not x is Filter of L or not a in
x) by Th18;
hence thesis;
end;
theorem
Th20: for Z st Z <> {} & Z c= SF_have b \ SF_have a &
Z is c=-linear
ex Y st Y in SF_have b \ SF_have a & for X1 st X1 in Z holds X1 c= Y
proof
let Z;
assume A1: Z <> {} & Z c= SF_have b \ SF_have a & Z is c=-linear;
then Z c= bool the carrier of L by XBOOLE_1:1;
then reconsider Z as Subset-Family of L
by SETFAM_1:def 7;
take Y = union Z;
Y in SF_have b \ SF_have a
proof
A2: not a in Y
proof
assume a in Y;
then consider X such that
A3: a in X & X in Z by TARSKI:def 4;
thus contradiction by A1,A3,Th19;
end;
consider X being Element of Z;
X in SF_have b \ SF_have a by A1,TARSKI:def 3;
then A4: b in X by Th19;
then A5: b in Y by A1,TARSKI:def 4;
reconsider Y as non empty Subset of L by A1,A4,TARSKI:def
4;
Y is Filter of L
proof
let p,q be Element of L;
thus p in Y & q in Y implies p "/\" q in Y
proof
assume p in Y;
then consider X1 such that
A6: p in X1 & X1 in Z by TARSKI:def 4;
assume q in Y;
then consider X2 such that
A7: q in X2 & X2 in Z by TARSKI:def 4;
A8: X1,X2 are_c=-comparable & X1 is Filter of L &
X2 is Filter of L by A1,A6,A7,Th19,ORDINAL1:def 9;
then X1 c= X2 or X2 c= X1 by XBOOLE_0:def 9;
then p "/\" q in X1 or p "/\" q in X2 by A6,A7,A8,FILTER_0:def 1;
hence thesis by A6,A7,TARSKI:def 4;
end;
assume p "/\" q in Y;
then consider X1 such that
A9: p "/\" q in X1 & X1 in Z by TARSKI:def 4;
X1 is Filter of L by A1,A9,Th19;
then p in X1 & q in X1 by A9,FILTER_0:def 1;
hence thesis by A9,TARSKI:def 4;
end;
hence thesis by A2,A5,Lm3;
end;
hence thesis by ZFMISC_1:92;
end;
theorem
Th21: not b [= a implies <.b.) in SF_have b \ SF_have a
proof
assume A1: not b [= a;
b in <.b.) by FILTER_0:19;
then A2: <.b.) in SF_have b by Th18;
not a in <.b.) by A1,FILTER_0:18;
then not <.b.) in SF_have a by Th18;
hence <.b.) in SF_have b \ SF_have a by A2,XBOOLE_0:def 4;
end;
theorem
Th22: not b [= a implies ex F st (F in F_primeSet(L) & not a in F & b in F )
proof
assume A1: not b [= a;
set A = SF_have b \ SF_have a;
A2: A <> {} by A1,Th21;
for Z st Z <> {} & Z c= SF_have b \ SF_have a & Z is c=-linear
ex Y st Y in SF_have b\ SF_have a & for X1 st X1 in Z holds X1 c= Y
by Th20;
then consider Y such that
A3: Y in A & for Z st Z in
A & Z <> Y holds not Y c= Z by A2,LATTICE4:3;
reconsider Y as Filter of L by A3,Th19;
A4: not a in Y & b in Y by A3,Th19;
A5: Y <> the carrier of L by A3,Th19;
Y is prime
proof
let a1,a2 be Element of L;
thus a1"\/"a2 in Y implies a1 in Y or a2 in Y
proof
assume A6: a1"\/"a2 in Y & not a1 in Y & not a2 in Y;
set F1=<.<.a1.) \/ Y.);
set F2=<.<.a2.) \/ Y.);
A7: not a in F1 or not a in F2
proof
assume A8: a in F1 & a in F2;
then consider c1 being Element of L such that
A9: c1 in Y & a1 "/\" c1 [= a by LATTICE4:6;
consider c2 being Element of L such that
A10: c2 in Y & a2 "/\" c2 [= a by A8,LATTICE4:6;
set c = c1 "/\" c2;
A11: c in Y by A9,A10,FILTER_0:def 1;
c [= c1 & c [= c2 by LATTICES:23;
then a1 "/\" c [= a1 "/\" c1 & a2 "/\" c [= a2 "/\"
c2 by LATTICES:27;
then a1 "/\" c [= a & a2 "/\" c [= a by A9,A10,LATTICES:25;
then (a1 "/\" c) "\/"( a2 "/\" c) [= a by FILTER_0:6;
then A12: (a1 "\/" a2) "/\" c [= a by LATTICES:def 11;
(a1 "\/" a2) "/\" c in Y by A6,A11,FILTER_0:def 1;
hence contradiction by A4,A12,FILTER_0:9;
end;
A13: a1 in <.a1.) & a2 in <.a2.) by FILTER_0:19;
<.a1.) c= F1 & <.a2.) c= F2 by LATTICE4:5;
then A14: a1 in F1 & a2 in F2 by A13;
A15: Y c= F1 & Y c= F2 by LATTICE4:5;
then F1 in A or F2 in A by A4,A7,Lm3;
hence contradiction by A3,A6,A14,A15;
end;
thus thesis by FILTER_0:10;
end;
then Y in F_primeSet(L) by A5,Th12;
hence thesis by A4;
end;
theorem
Th23: a <> b implies ex F st F in F_primeSet(L)
proof
assume a <> b;
then not a [= b or not b [= a by LATTICES:26;
then (ex F st F in F_primeSet(L) & not b in F & a in F) or
( ex F st F in F_primeSet(L) & not a in F & b in F) by Th22;
then consider F such that
A1: F in F_primeSet(L) & ( b in F & not a in F or a in F);
thus thesis by A1;
end;
theorem
Th24: a <> b implies StoneH(L).a <> StoneH(L).b
proof
assume a <> b;
then not a [= b or not b [= a by LATTICES:26;
then (ex F st F in F_primeSet(L) & not b in F & a in F) or
( ex F st F in F_primeSet(L) & not a in F & b in F ) by Th22;
then consider F such that
A1: F in F_primeSet(L) & ( b in F & not a in F or a in F & not b in F);
F in StoneH(L).a & not F in StoneH(L).b or
F in StoneH(L).b & not F in StoneH(L).a by A1,Th13;
hence thesis;
end;
theorem
Th25: StoneH(L) is one-to-one
proof
let x1,x2 be set;
assume that
A1: x1 in dom StoneH(L) & x2 in dom StoneH(L) and
A2: StoneH(L).x1 = StoneH(L).x2;
reconsider a1=x1,a2=x2 as Element of L by A1,Def6;
a1=a2 by A2,Th24;
hence x1 = x2;
end;
definition let L;let A,B be Element of StoneS(L);
redefine func A \/ B -> Element of StoneS(L);
coherence
proof
consider a such that
A1: A = StoneH(L).a by Th15;
consider b such that
A2: B = StoneH(L).b by Th15;
A \/ B = StoneH(L).(a "\/" b) by A1,A2,Th16;
hence A \/ B is Element of StoneS(L) by Th15;
end;
redefine func A /\ B -> Element of StoneS(L);
coherence
proof
consider a such that
A3: A = StoneH(L).a by Th15;
consider b such that
A4: B = StoneH(L).b by Th15;
A /\ B = StoneH(L).(a "/\" b) by A3,A4,Th17;
hence A /\ B is Element of StoneS(L) by Th15;
end;
end;
definition let L;
func Set_Union L -> BinOp of StoneS(L) means
:Def9: for A,B being Element of StoneS(L) holds it.(A,B) = A \/ B;
existence
proof
deffunc F(Element of StoneS(L), Element of StoneS(L)) = $1 \/ $2;
thus ex F being BinOp of StoneS(L) st
for P,Q being Element of StoneS(L) holds
F.(P,Q) = F(P,Q) from BinOpLambda;
end;
uniqueness
proof
set A = StoneS(L);
deffunc O(Element of A, Element of A) = $1 \/ $2;
thus for o1,o2 being BinOp of A st
(for a,b being Element of A holds o1.(a,b) = O(a,b)) &
(for a,b being Element of A holds o2.(a,b) = O(a,b))
holds o1 = o2 from BinOpDefuniq;
end;
func Set_Meet L -> BinOp of StoneS(L) means
:Def10: for A,B being Element of StoneS(L) holds it.(A,B) = A /\ B;
existence
proof
deffunc F(Element of StoneS(L), Element of StoneS(L)) = $1 /\ $2;
thus ex F being BinOp of StoneS(L) st
for P,Q being Element of StoneS(L) holds
F.(P,Q) = F(P,Q) from BinOpLambda;
end;
uniqueness
proof
set A = StoneS(L);
deffunc O(Element of A, Element of A) = $1 /\ $2;
thus for o1,o2 being BinOp of A st
(for a,b being Element of A holds o1.(a,b) = O(a,b)) &
(for a,b being Element of A holds o2.(a,b) = O(a,b))
holds o1 = o2 from BinOpDefuniq;
end;
end;
Lm4: for x,y be Element of
LattStr(#StoneS(L),Set_Union L,Set_Meet L#) holds x"\/"y = x \/ y
proof
let x,y be Element of
LattStr(#StoneS(L),Set_Union L,Set_Meet L#);
reconsider x'=x,y'=y as Element of StoneS(L);
thus x"\/"y = (Set_Union L).(x',y') by LATTICES:def 1
.= x \/ y by Def9;
end;
Lm5: for x,y be Element of
LattStr(#StoneS(L),Set_Union L,Set_Meet L#) holds x"/\"y = x /\ y
proof
let x,y be Element of
LattStr(#StoneS(L),Set_Union L,Set_Meet L#);
reconsider x'=x,y'=y as Element of StoneS(L);
thus x"/\"y = (Set_Meet L).(x',y') by LATTICES:def 2
.= x /\ y by Def10;
end;
theorem
Th26: LattStr(#StoneS(L),Set_Union L,Set_Meet L#) is Lattice
proof
set SL = LattStr(#StoneS(L),Set_Union L,Set_Meet L#);
A1: now let p,q be Element of SL;
thus p "\/" q = q \/ p by Lm4
.= q"\/"p by Lm4;
end;
A2: now let p,q,r be Element of SL;
thus p"\/"(q"\/"r) = p \/ (q "\/" r) by Lm4
.= p \/ (q \/ r) by Lm4
.= (p \/ q) \/ r by XBOOLE_1:4
.= (p "\/" q) \/ r by Lm4
.= (p"\/"q)"\/"r by Lm4;
end;
A3: now let p,q be Element of SL;
thus (p"/\"q)"\/"q = (p"/\"q) \/ q by Lm4
.= (p /\ q) \/ q by Lm5
.= q by XBOOLE_1:22;
end;
A4: now let p,q be Element of SL;
thus p "/\" q =q /\ p by Lm5
.= q"/\"p by Lm5;
end;
A5: now let p,q,r be Element of SL;
thus p"/\"(q"/\"r) = p /\ (q "/\" r) by Lm5
.= p /\ (q /\ r) by Lm5
.= (p /\ q) /\ r by XBOOLE_1:16
.= (p "/\" q) /\ r by Lm5
.= (p"/\"q)"/\"r by Lm5;
end;
now let p,q be Element of SL;
thus p"/\"(p"\/"q) = p /\ (p"\/"q) by Lm5
.= p /\ (p \/ q) by Lm4
.= p by XBOOLE_1:21;
end;
then SL is join-commutative join-associative meet-absorbing
meet-commutative meet-associative join-absorbing
by A1,A2,A3,A4,A5,LATTICES:def 4,def 5,def 6,def 7,def 8,def 9;
hence SL is Lattice by LATTICES:def 10;
end;
definition let L;
func StoneLatt L -> Lattice equals
:Def11: LattStr(#StoneS(L),Set_Union L,Set_Meet L#);
coherence by Th26;
end;
reserve p,q for Element of StoneLatt(L);
theorem
Th27: for L holds the carrier of StoneLatt(L) = StoneS(L)
proof
let L;
StoneLatt(L)=LattStr(#StoneS(L),Set_Union L,Set_Meet L#) by Def11;
hence thesis;
end;
theorem
Th28: p "\/" q = p \/ q & p "/\" q = p /\ q
proof
A1: StoneLatt(L)=LattStr(#StoneS(L),Set_Union L,Set_Meet L#) by Def11;
hence p "\/" q = p \/ q by Lm4;
thus p "/\" q = p /\ q by A1,Lm5;
end;
theorem
p [= q iff p c= q
proof
(p [= q iff p "\/" q = q) & p "\/" q = p \/ q by Th28,LATTICES:def 3;
hence thesis by XBOOLE_1:7,12;
end;
definition let L;
redefine func StoneH(L) -> Homomorphism of L,StoneLatt L;
coherence
proof
A1: dom StoneH(L) = the carrier of L by Def6;
rng StoneH(L) = StoneS(L) by Def7
.= the carrier of StoneLatt(L) by Th27;
then reconsider f=StoneH(L) as Function of the carrier of L ,
the carrier of StoneLatt L by A1,FUNCT_2:3;
now let a,b;
thus f.(a "\/" b) = f.(a) \/ f.(b) by Th16
.=f.a "\/" f.b by Th28;
thus f.(a "/\" b) = f.(a) /\ f.(b) by Th17
.=f.(a) "/\" f.(b) by Th28;
end;
hence thesis by LATTICE4:def 1;
end;
end;
theorem
Th30: StoneH(L) is isomorphism
proof
thus StoneH(L) is one-to-one by Th25;
thus rng StoneH(L) = StoneS(L) by Def7
.= the carrier of StoneLatt L by Th27;
end;
theorem
StoneLatt(L) is distributive
proof
StoneH(L) is isomorphism by Th30;
then StoneH(L) is epimorphism by LATTICE4:def 4;
hence thesis by LATTICE4:18;
end;
theorem
L,StoneLatt L are_isomorphic
proof
take StoneH(L);
thus thesis by Th30;
end;
definition
cluster non trivial H_Lattice;
existence
proof consider T;
set OL=Open_setLatt(T);
the carrier of T = Top OL by Th11;
then reconsider a= the carrier of T as Element of OL;
{} = Bottom OL by Th10;
then reconsider b= {} as Element of OL;
take OL,a,b;
thus a <> b;
end;
end;
reserve H for non trivial H_Lattice;
reserve p',q' for Element of H;
theorem
Th33: StoneH(H).(Top H) = F_primeSet(H)
proof
hereby let x;
assume x in StoneH(H).(Top H);
then consider F being Filter of H such that
A1: F=x & F <> the carrier of H & F is prime & Top H in F by Th14;
thus x in F_primeSet(H) by A1,Th12;
end;
let x;
assume A2:x in F_primeSet(H);
F_primeSet(H)={F0 where F0 is Filter of H:
F0 <> the carrier of H & F0 is prime} by Def5;
then consider F being Filter of H such that
A3: F=x & F <> the carrier of H & F is prime by A2;
Top H in F by FILTER_0:12;
hence x in StoneH(H).(Top H) by A3,Th14;
end;
theorem
Th34: StoneH(H).(Bottom H) = {}
proof
assume
A1: StoneH(H).(Bottom H) <> {};
consider x being Element of StoneH(H).(Bottom H);
consider F being Filter of H such that
A2: F=x & F <> the carrier of H & F is prime & Bottom
H in F by A1,Th14;
thus contradiction by A2,FILTER_0:32;
end;
theorem
Th35: StoneS(H) c= bool F_primeSet(H)
proof
let x;
assume x in StoneS(H);
then consider p' such that
A1: x=StoneH(H).p' by Th15;
A2: x={F where F is Filter of H:F in F_primeSet(H) & p' in
F} by A1,Def6;
x c= F_primeSet(H)
proof
let y be set;
assume y in x;
then consider F being Filter of H such that
A3: y=F & F in F_primeSet(H) & p' in F by A2;
thus y in F_primeSet(H) by A3;
end;
hence x in bool F_primeSet(H);
end;
definition let H;
cluster F_primeSet(H) -> non empty;
coherence
proof
consider p',q' such that
A1: p' <> q' by REALSET1:def 20;
ex F being Filter of H st F in F_primeSet(H) by A1,Th23;
hence thesis;
end;
end;
definition let H;
func HTopSpace H -> strict TopStruct means
:Def12: the carrier of it = F_primeSet(H) &
the topology of it ={union A where A is Subset of StoneS(H):not
contradiction};
existence
proof
set top={union A where A is Subset of StoneS(H):not contradiction};
set FS= F_primeSet(H);
A1: StoneS(H) c= bool FS by Th35;
top c= bool FS
proof
let x;
assume x in top;
then consider A being Subset of StoneS(H) such that
A2: x=union A;
A c= bool FS by A1,XBOOLE_1:1;
then x c= union bool FS by A2,ZFMISC_1:95;
then x is Subset of FS by ZFMISC_1:99;
hence x in bool FS;
end;
then reconsider top as Subset-Family of FS by SETFAM_1:def 7;
take TopStruct(#FS ,top#);
thus thesis;
end;
uniqueness;
end;
definition let H;
cluster HTopSpace H -> non empty TopSpace-like;
coherence
proof
set TS = HTopSpace H;
A1: the carrier of TS = F_primeSet(H) by Def12;
A2: the topology of TS ={union A where A is Subset of StoneS(H):not
contradiction} by Def12;
thus HTopSpace H is non empty
proof
thus the carrier of HTopSpace H is non empty by A1;
end;
StoneH(H).(Top H) in StoneS(H) by Th15;
then reconsider A1={StoneH(H).(Top
H)} as Subset of StoneS(H) by ZFMISC_1:37;
F_primeSet(H) = StoneH(H).(Top H) by Th33;
then F_primeSet(H)=union A1 by ZFMISC_1:31;
hence the carrier of TS in the topology of TS by A1,A2;
hereby let a be Subset-Family of TS;
defpred P[set] means union $1 in a;
set B= {A where A is Subset of StoneS(H) :P[A]};
assume A3: a c= the topology of TS;
set X= {union A where A is Subset of StoneS(H) : A in B};
A4: a = X
proof
hereby let x;
assume A5:x in a;
then x in the topology of TS by A3;
then consider A be Subset of StoneS(H) such that
A6: x=union A by A2;
A in B by A5,A6;
hence x in X by A6;
end;
let x;
assume x in X;
then consider A be Subset of StoneS(H) such that
A7: x=union A & A in B;
ex A' be Subset of StoneS(H) st A=A' & union A' in a by A7;
hence thesis by A7;
end;
reconsider B as Subset of bool StoneS(H) from SubsetD;
reconsider B as Subset-Family of StoneS(H) by SETFAM_1:def 7;
union union B = union a by A4,BORSUK_1:17;
hence union a in the topology of TS by A2;
end;
let a,b be Subset of TS;
assume A8: a in the topology of TS & b in the topology of TS;
then consider A being Subset of StoneS(H) such that
A9: a = union A by A2;
consider B being Subset of StoneS(H) such that
A10: b = union B by A2,A8;
INTERSECTION(A,B) c= StoneS(H)
proof
let x;
assume x in INTERSECTION(A,B);
then consider X,Y being set such that
A11: X in A & Y in B & x = X /\ Y by SETFAM_1:def 5;
consider p' such that
A12: X=StoneH(H).p' by A11,Th15;
consider q' such that
A13: Y=StoneH(H).q' by A11,Th15;
x = StoneH(H).(p' "/\" q') by A11,A12,A13,Th17;
hence x in StoneS(H) by Th15;
end;
then reconsider C=INTERSECTION(A,B) as Subset of StoneS(H);
union A /\ union B = union C by LATTICE4:2;
hence a /\ b in the topology of TS by A2,A9,A10;
end;
end;
theorem
Th36: the carrier of Open_setLatt(HTopSpace H) =
{union A where A is Subset of StoneS(H):not contradiction}
proof
set HT=HTopSpace H;
Open_setLatt(HT)=
LattStr(#Topology_of HT,Top_Union HT,Top_Meet HT#) by Def4;
hence the carrier of Open_setLatt(HT) = the topology of HT by Def1
.= {union A where A is Subset of StoneS(H):not contradiction} by Def12;
end;
theorem
Th37: StoneS(H) c= the carrier of Open_setLatt(HTopSpace H)
proof
let x;
assume A1: x in StoneS(H);
set carrO = the carrier of Open_setLatt(HTopSpace H);
A2: carrO = {union A where A is Subset of StoneS(H):not contradiction}
by Th36;
reconsider z={x} as Subset of StoneS(H) by A1,ZFMISC_1:37;
union z = x by ZFMISC_1:31;
hence x in carrO by A2;
end;
definition let H;
redefine func StoneH(H) -> Homomorphism of H,Open_setLatt(HTopSpace H);
coherence
proof
reconsider g=StoneH(H) as Function of the carrier of H,
the carrier of StoneLatt(H);
set LH=Open_setLatt(HTopSpace H);
StoneS(H) c= the carrier of LH by Th37;
then rng StoneH(H) c= the carrier of LH by Def7;
then reconsider f=g as Function of the carrier of H,
the carrier of LH by FUNCT_2:8;
now let p',q';
thus f.(p' "\/" q') = StoneH(H).p' \/ StoneH(H).q' by Th16
.= f.p' "\/" f.q' by Th6;
thus f.(p' "/\" q') = StoneH(H).p' /\ StoneH(H).q' by Th17
.= f.p' "/\" f.q' by Th6;
end;
hence thesis by LATTICE4:def 1;
end;
end;
theorem
Th38: StoneH(H) is monomorphism
proof
StoneH(H) is one-to-one by Th25;
hence thesis by LATTICE4:def 2;
end;
theorem
Th39: StoneH(H).(p' => q') = (StoneH(H).p') => (StoneH(H).q')
proof
A1: StoneH(H) is monomorphism by Th38;
A2: the carrier of Open_setLatt(HTopSpace H) =
{union A where A is Subset of StoneS(H):not contradiction} by Th36;
p' "/\" (p' => q') [= q' by FILTER_0:def 8;
then StoneH(H).(p' "/\" (p' => q')) [= StoneH(H).q' by LATTICE4:7;
then A3: StoneH(H).p'"/\"
StoneH(H).(p' => q') [= StoneH(H).q' by LATTICE4:def 1;
now let r be Element of Open_setLatt(HTopSpace H);
assume A4: StoneH(H).p' "/\" r [= StoneH(H).q';
r in the carrier of Open_setLatt(HTopSpace H);
then consider A being Subset of StoneS(H) such that
A5: r = union A by A2;
StoneH(H).p' "/\" r c= StoneH(H).q' by A4,Th7;
then StoneH(H).p' /\ union A c= StoneH(H).q' by A5,Th6;
then A6: union INTERSECTION ({StoneH(H).p'}, A) c= StoneH(H).q'
by SETFAM_1:36;
now let x;
assume A7: x in A;
then consider x' being Element of H such that
A8: x=StoneH(H).x' by Th15;
StoneH(H).p' in {StoneH(H).p'} by TARSKI:def 1;
then StoneH(H).p' /\ x in INTERSECTION ({StoneH(H).p'}, A)
by A7,SETFAM_1:def 5;
then StoneH(H).p' /\ StoneH(H).x' c= StoneH(H).q'
by A6,A8,LATTICE4:1;
then StoneH(H).(p' "/\" x') c= StoneH(H).q' by Th17;
then StoneH(H).(p' "/\" x') [= StoneH(H).q' by Th7;
then (p' "/\" x') [= q' by A1,LATTICE4:8;
then x' [= p' => q' by FILTER_0:def 8;
then StoneH(H).x' [= StoneH(H).(p' => q') by LATTICE4:7;
hence x c= StoneH(H).(p' => q') by A8,Th7;
end;
then union A c= StoneH(H).(p' => q') by ZFMISC_1:94;
hence r [= StoneH(H).(p' => q') by A5,Th7;
end;
hence thesis by A3,FILTER_0:def 8;
end;
theorem
StoneH(H) preserves_implication
proof
for p',q' holds
StoneH(H).(p' => q') = (StoneH(H).p') => (StoneH(H).q') by Th39;
hence thesis by LATTICE4:def 6;
end;
theorem
StoneH(H) preserves_top
proof
StoneH(H).(Top H) = F_primeSet(H) by Th33
.= the carrier of HTopSpace H by Def12
.= Top (Open_setLatt(HTopSpace H)) by Th11;
hence thesis by LATTICE4:def 7;
end;
theorem
StoneH(H) preserves_bottom
proof
StoneH(H).(Bottom H) = {} by Th34
.= Bottom (Open_setLatt(HTopSpace H)) by Th10;
hence thesis by LATTICE4:def 8;
end;