:: OPENLATT semantic presentation
begin
registration
cluster non empty Lattice-like lower-bounded Heyting -> implicative for LattStr ;
coherence
for b1 being 0_Lattice st b1 is Heyting holds
b1 is implicative ;
cluster non empty Lattice-like implicative -> upper-bounded for LattStr ;
coherence
for b1 being Lattice st b1 is implicative holds
b1 is upper-bounded ;
end;
theorem Th1: :: OPENLATT:1
for T being TopSpace
for A, B being Subset of T holds A /\ (Int ((A `) \/ B)) c= B
proof
let T be TopSpace; ::_thesis: for A, B being Subset of T holds A /\ (Int ((A `) \/ B)) c= B
let A, B be Subset of T; ::_thesis: A /\ (Int ((A `) \/ B)) c= B
A1: A misses A ` by XBOOLE_1:79;
A /\ ((A `) \/ B) = (A /\ (A `)) \/ (A /\ B) by XBOOLE_1:23
.= {} \/ (A /\ B) by A1, XBOOLE_0:def_7
.= A /\ B ;
then A2: A /\ ((A `) \/ B) c= B by XBOOLE_1:17;
A /\ (Int ((A `) \/ B)) c= A /\ ((A `) \/ B) by TOPS_1:16, XBOOLE_1:26;
hence A /\ (Int ((A `) \/ B)) c= B by A2, XBOOLE_1:1; ::_thesis: verum
end;
theorem Th2: :: OPENLATT:2
for T being TopSpace
for A, B, C being Subset of T st C is open & A /\ C c= B holds
C c= Int ((A `) \/ B)
proof
let T be TopSpace; ::_thesis: for A, B, C being Subset of T st C is open & A /\ C c= B holds
C c= Int ((A `) \/ B)
let A, B, C be Subset of T; ::_thesis: ( C is open & A /\ C c= B implies C c= Int ((A `) \/ B) )
assume that
A1: C is open and
A2: A /\ C c= B ; ::_thesis: C c= Int ((A `) \/ B)
A3: 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:2
.= C \/ (A `) by XBOOLE_1:28 ;
then C \/ (A `) c= B \/ (A `) by A2, XBOOLE_1:9;
then C c= B \/ (A `) by A3, XBOOLE_1:1;
then Int C c= Int ((A `) \/ B) by TOPS_1:19;
hence C c= Int ((A `) \/ B) by A1, TOPS_1:23; ::_thesis: verum
end;
definition
let T be TopStruct ;
func Topology_of T -> Subset-Family of T equals :: OPENLATT:def 1
the topology of T;
coherence
the topology of T is Subset-Family of T ;
end;
:: deftheorem defines Topology_of OPENLATT:def_1_:_
for T being TopStruct holds Topology_of T = the topology of T;
registration
let T be TopSpace;
cluster Topology_of T -> non empty ;
coherence
not Topology_of T is empty ;
end;
definition
let T be non empty TopSpace;
let P, Q be Element of Topology_of T;
:: original: \/
redefine funcP \/ Q -> Element of Topology_of T;
coherence
P \/ Q is Element of Topology_of T
proof
reconsider A = P, B = Q as Subset of T ;
A1: B is open by PRE_TOPC:def_2;
A is open by PRE_TOPC:def_2;
then P \/ Q is open by A1;
hence P \/ Q is Element of Topology_of T by PRE_TOPC:def_2; ::_thesis: verum
end;
:: original: /\
redefine funcP /\ Q -> Element of Topology_of T;
coherence
P /\ Q is Element of Topology_of T
proof
reconsider A = P, B = Q as Subset of T ;
A2: B is open by PRE_TOPC:def_2;
A is open by PRE_TOPC:def_2;
then P /\ Q is open by A2;
hence P /\ Q is Element of Topology_of T by PRE_TOPC:def_2; ::_thesis: verum
end;
end;
definition
let T be non empty TopSpace;
func Top_Union T -> BinOp of (Topology_of T) means :Def2: :: OPENLATT:def 2
for P, Q being Element of Topology_of T holds it . (P,Q) = P \/ Q;
existence
ex b1 being BinOp of (Topology_of T) st
for P, Q being Element of Topology_of T holds b1 . (P,Q) = P \/ Q
proof
deffunc H1( Element of Topology_of T, 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) = H1(P,Q) from BINOP_1:sch_4(); ::_thesis: verum
end;
uniqueness
for b1, b2 being BinOp of (Topology_of T) st ( for P, Q being Element of Topology_of T holds b1 . (P,Q) = P \/ Q ) & ( for P, Q being Element of Topology_of T holds b2 . (P,Q) = P \/ Q ) holds
b1 = b2
proof
set A = Topology_of T;
deffunc H1( Element of Topology_of T, Element of Topology_of T) -> Element of Topology_of T = $1 \/ $2;
thus for o1, o2 being BinOp of (Topology_of T) st ( for a, b being Element of Topology_of T holds o1 . (a,b) = H1(a,b) ) & ( for a, b being Element of Topology_of T holds o2 . (a,b) = H1(a,b) ) holds
o1 = o2 from BINOP_2:sch_2(); ::_thesis: verum
end;
func Top_Meet T -> BinOp of (Topology_of T) means :Def3: :: OPENLATT:def 3
for P, Q being Element of Topology_of T holds it . (P,Q) = P /\ Q;
existence
ex b1 being BinOp of (Topology_of T) st
for P, Q being Element of Topology_of T holds b1 . (P,Q) = P /\ Q
proof
deffunc H1( Element of Topology_of T, 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) = H1(P,Q) from BINOP_1:sch_4(); ::_thesis: verum
end;
uniqueness
for b1, b2 being BinOp of (Topology_of T) st ( for P, Q being Element of Topology_of T holds b1 . (P,Q) = P /\ Q ) & ( for P, Q being Element of Topology_of T holds b2 . (P,Q) = P /\ Q ) holds
b1 = b2
proof
set A = Topology_of T;
deffunc H1( Element of Topology_of T, Element of Topology_of T) -> Element of Topology_of T = $1 /\ $2;
thus for o1, o2 being BinOp of (Topology_of T) st ( for a, b being Element of Topology_of T holds o1 . (a,b) = H1(a,b) ) & ( for a, b being Element of Topology_of T holds o2 . (a,b) = H1(a,b) ) holds
o1 = o2 from BINOP_2:sch_2(); ::_thesis: verum
end;
end;
:: deftheorem Def2 defines Top_Union OPENLATT:def_2_:_
for T being non empty TopSpace
for b2 being BinOp of (Topology_of T) holds
( b2 = Top_Union T iff for P, Q being Element of Topology_of T holds b2 . (P,Q) = P \/ Q );
:: deftheorem Def3 defines Top_Meet OPENLATT:def_3_:_
for T being non empty TopSpace
for b2 being BinOp of (Topology_of T) holds
( b2 = Top_Meet T iff for P, Q being Element of Topology_of T holds b2 . (P,Q) = P /\ Q );
theorem Th3: :: OPENLATT:3
for T being non empty TopSpace holds LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) is Lattice
proof
let T be non empty TopSpace; ::_thesis: LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) is Lattice
set L = LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #);
A1: now__::_thesis:_for_p,_q_being_Element_of_LattStr(#_(Topology_of_T),(Top_Union_T),(Top_Meet_T)_#)_holds_p_"\/"_q_=_q_"\/"_p
let p, q be Element of LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #); ::_thesis: p "\/" q = q "\/" p
thus p "\/" q = q \/ p by Def2
.= q "\/" p by Def2 ; ::_thesis: verum
end;
A2: now__::_thesis:_for_p,_q_being_Element_of_LattStr(#_(Topology_of_T),(Top_Union_T),(Top_Meet_T)_#)_holds_(p_"/\"_q)_"\/"_q_=_q
let p, q be Element of LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #); ::_thesis: (p "/\" q) "\/" q = q
thus (p "/\" q) "\/" q = (p "/\" q) \/ q by Def2
.= (p /\ q) \/ q by Def3
.= q by XBOOLE_1:22 ; ::_thesis: verum
end;
A3: now__::_thesis:_for_p,_q_being_Element_of_LattStr(#_(Topology_of_T),(Top_Union_T),(Top_Meet_T)_#)_holds_p_"/\"_(p_"\/"_q)_=_p
let p, q be Element of LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #); ::_thesis: p "/\" (p "\/" q) = p
thus p "/\" (p "\/" q) = p /\ (p "\/" q) by Def3
.= p /\ (p \/ q) by Def2
.= p by XBOOLE_1:21 ; ::_thesis: verum
end;
A4: now__::_thesis:_for_p,_q,_r_being_Element_of_LattStr(#_(Topology_of_T),(Top_Union_T),(Top_Meet_T)_#)_holds_p_"/\"_(q_"/\"_r)_=_(p_"/\"_q)_"/\"_r
let p, q, r be Element of LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #); ::_thesis: p "/\" (q "/\" r) = (p "/\" q) "/\" r
thus p "/\" (q "/\" r) = p /\ (q "/\" r) by Def3
.= p /\ (q /\ r) by Def3
.= (p /\ q) /\ r by XBOOLE_1:16
.= (p "/\" q) /\ r by Def3
.= (p "/\" q) "/\" r by Def3 ; ::_thesis: verum
end;
A5: now__::_thesis:_for_p,_q_being_Element_of_LattStr(#_(Topology_of_T),(Top_Union_T),(Top_Meet_T)_#)_holds_p_"/\"_q_=_q_"/\"_p
let p, q be Element of LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #); ::_thesis: p "/\" q = q "/\" p
thus p "/\" q = q /\ p by Def3
.= q "/\" p by Def3 ; ::_thesis: verum
end;
now__::_thesis:_for_p,_q,_r_being_Element_of_LattStr(#_(Topology_of_T),(Top_Union_T),(Top_Meet_T)_#)_holds_p_"\/"_(q_"\/"_r)_=_(p_"\/"_q)_"\/"_r
let p, q, r be Element of LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #); ::_thesis: p "\/" (q "\/" r) = (p "\/" q) "\/" r
thus p "\/" (q "\/" r) = p \/ (q "\/" r) by Def2
.= p \/ (q \/ r) by Def2
.= (p \/ q) \/ r by XBOOLE_1:4
.= (p "\/" q) \/ r by Def2
.= (p "\/" q) "\/" r by Def2 ; ::_thesis: verum
end;
then ( LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) is join-commutative & LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) is join-associative & LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) is meet-absorbing & LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) is meet-commutative & LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) is meet-associative & LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) is join-absorbing ) by A1, A2, A5, A4, A3, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9;
hence LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) is Lattice ; ::_thesis: verum
end;
definition
let T be non empty TopSpace;
func Open_setLatt T -> Lattice equals :: OPENLATT:def 4
LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #);
coherence
LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) is Lattice by Th3;
end;
:: deftheorem defines Open_setLatt OPENLATT:def_4_:_
for T being non empty TopSpace holds Open_setLatt T = LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #);
theorem :: OPENLATT:4
for T being non empty TopSpace holds the carrier of (Open_setLatt T) = Topology_of T ;
theorem :: OPENLATT:5
for T being non empty TopSpace
for p, q being Element of (Open_setLatt T) holds
( p "\/" q = p \/ q & p "/\" q = p /\ q ) by Def2, Def3;
theorem Th6: :: OPENLATT:6
for T being non empty TopSpace
for p, q being Element of (Open_setLatt T) holds
( p [= q iff p c= q )
proof
let T be non empty TopSpace; ::_thesis: for p, q being Element of (Open_setLatt T) holds
( p [= q iff p c= q )
let p, q be Element of (Open_setLatt T); ::_thesis: ( p [= q iff p c= q )
A1: ( p [= q iff p "\/" q = q ) by LATTICES:def_3;
p "\/" q = p \/ q by Def2;
hence ( p [= q iff p c= q ) by A1, XBOOLE_1:7, XBOOLE_1:12; ::_thesis: verum
end;
theorem Th7: :: OPENLATT:7
for T being non empty TopSpace
for p, q being Element of (Open_setLatt T)
for p9, q9 being Element of Topology_of T st p = p9 & q = q9 holds
( p [= q iff p9 c= q9 )
proof
let T be non empty TopSpace; ::_thesis: for p, q being Element of (Open_setLatt T)
for p9, q9 being Element of Topology_of T st p = p9 & q = q9 holds
( p [= q iff p9 c= q9 )
let p, q be Element of (Open_setLatt T); ::_thesis: for p9, q9 being Element of Topology_of T st p = p9 & q = q9 holds
( p [= q iff p9 c= q9 )
let p9, q9 be Element of Topology_of T; ::_thesis: ( p = p9 & q = q9 implies ( p [= q iff p9 c= q9 ) )
assume that
A1: p = p9 and
A2: q = q9 ; ::_thesis: ( p [= q iff p9 c= q9 )
hereby ::_thesis: ( p9 c= q9 implies p [= q )
assume A3: p [= q ; ::_thesis: p9 c= q9
p9 \/ q9 = p "\/" q by A1, A2, Def2
.= q9 by A2, A3, LATTICES:def_3 ;
hence p9 c= q9 by XBOOLE_1:7; ::_thesis: verum
end;
assume A4: p9 c= q9 ; ::_thesis: p [= q
p "\/" q = p9 \/ q9 by A1, A2, Def2
.= q by A2, A4, XBOOLE_1:12 ;
hence p [= q by LATTICES:def_3; ::_thesis: verum
end;
registration
let T be non empty TopSpace;
cluster Open_setLatt T -> implicative ;
coherence
Open_setLatt T is implicative
proof
set OL = Open_setLatt T;
let p, q be Element of (Open_setLatt T); :: according to FILTER_0:def_6 ::_thesis: ex b1 being Element of the carrier of (Open_setLatt T) st
( p "/\" b1 [= q & ( for b2 being Element of the carrier of (Open_setLatt T) holds
( not p "/\" b2 [= q or b2 [= b1 ) ) )
reconsider p9 = p, q9 = q as Element of Topology_of T ;
reconsider r9 = Int ((p9 `) \/ q9) as Element of Topology_of T by PRE_TOPC:def_2;
reconsider r = r9 as Element of (Open_setLatt T) ;
take r ; ::_thesis: ( p "/\" r [= q & ( for b1 being Element of the carrier of (Open_setLatt T) holds
( not p "/\" b1 [= q or b1 [= r ) ) )
A1: p "/\" r = p9 /\ r9 by Def3;
p9 /\ r c= q9 by Th1;
hence p "/\" r [= q by A1, Th7; ::_thesis: for b1 being Element of the carrier of (Open_setLatt T) holds
( not p "/\" b1 [= q or b1 [= r )
let r1 be Element of (Open_setLatt T); ::_thesis: ( not p "/\" r1 [= q or r1 [= r )
reconsider r2 = r1 as Element of Topology_of T ;
reconsider r19 = r2 as Subset of T ;
A2: r19 is open by PRE_TOPC:def_2;
assume A3: p "/\" r1 [= q ; ::_thesis: r1 [= r
p "/\" r1 = p9 /\ r19 by Def3;
then p9 /\ r2 c= q9 by A3, Th7;
then r19 c= r9 by A2, Th2;
hence r1 [= r by Th7; ::_thesis: verum
end;
end;
theorem Th8: :: OPENLATT:8
for T being non empty TopSpace holds
( Open_setLatt T is lower-bounded & Bottom (Open_setLatt T) = {} )
proof
let T be non empty TopSpace; ::_thesis: ( Open_setLatt T is lower-bounded & Bottom (Open_setLatt T) = {} )
set OL = Open_setLatt T;
reconsider r = {} as Element of (Open_setLatt T) by PRE_TOPC:1;
A1: now__::_thesis:_for_p_being_Element_of_(Open_setLatt_T)_holds_
(_r_"/\"_p_=_r_&_p_"/\"_r_=_r_)
let p be Element of (Open_setLatt T); ::_thesis: ( r "/\" p = r & p "/\" r = r )
thus r "/\" p = r /\ p by Def3
.= r ; ::_thesis: p "/\" r = r
hence p "/\" r = r ; ::_thesis: verum
end;
thus Open_setLatt T is lower-bounded ::_thesis: Bottom (Open_setLatt T) = {}
proof
take r ; :: according to LATTICES:def_13 ::_thesis: for b1 being Element of the carrier of (Open_setLatt T) holds
( r "/\" b1 = r & b1 "/\" r = r )
thus for b1 being Element of the carrier of (Open_setLatt T) holds
( r "/\" b1 = r & b1 "/\" r = r ) by A1; ::_thesis: verum
end;
hence Bottom (Open_setLatt T) = {} by A1, LATTICES:def_16; ::_thesis: verum
end;
registration
let T be non empty TopSpace;
cluster Open_setLatt T -> Heyting ;
coherence
Open_setLatt T is Heyting
proof
reconsider OL = Open_setLatt T as 0_Lattice by Th8;
OL is I_Lattice ;
hence Open_setLatt T is Heyting ; ::_thesis: verum
end;
end;
theorem Th9: :: OPENLATT:9
for T being non empty TopSpace holds Top (Open_setLatt T) = the carrier of T
proof
let T be non empty TopSpace; ::_thesis: Top (Open_setLatt T) = the carrier of T
set OL = Open_setLatt T;
reconsider B = the carrier of T as Element of (Open_setLatt T) by PRE_TOPC:def_1;
now__::_thesis:_for_p_being_Element_of_(Open_setLatt_T)_holds_
(_B_"\/"_p_=_B_&_p_"\/"_B_=_B_)
let p be Element of (Open_setLatt T); ::_thesis: ( B "\/" p = B & p "\/" B = B )
reconsider p9 = p as Element of Topology_of T ;
thus B "\/" p = the carrier of T \/ p9 by Def2
.= B by XBOOLE_1:12 ; ::_thesis: p "\/" B = B
hence p "\/" B = B ; ::_thesis: verum
end;
hence Top (Open_setLatt T) = the carrier of T by LATTICES:def_17; ::_thesis: verum
end;
definition
let L be D_Lattice;
func F_primeSet L -> set equals :: OPENLATT:def 5
{ F where F is Filter of L : ( F <> the carrier of L & F is prime ) } ;
coherence
{ F where F is Filter of L : ( F <> the carrier of L & F is prime ) } is set ;
end;
:: deftheorem defines F_primeSet OPENLATT:def_5_:_
for L being D_Lattice holds F_primeSet L = { F where F is Filter of L : ( F <> the carrier of L & F is prime ) } ;
theorem Th10: :: OPENLATT:10
for L being D_Lattice
for F being Filter of L holds
( F in F_primeSet L iff ( F <> the carrier of L & F is prime ) )
proof
let L be D_Lattice; ::_thesis: for F being Filter of L holds
( F in F_primeSet L iff ( F <> the carrier of L & F is prime ) )
let F be Filter of L; ::_thesis: ( F in F_primeSet L iff ( F <> the carrier of L & F is prime ) )
( F in F_primeSet L iff ex F0 being Filter of L st
( F0 = F & F0 <> the carrier of L & F0 is prime ) ) ;
hence ( F in F_primeSet L iff ( F <> the carrier of L & F is prime ) ) ; ::_thesis: verum
end;
definition
let L be D_Lattice;
func StoneH L -> Function means :Def6: :: OPENLATT:def 6
for a being Element of L holds
( dom it = the carrier of L & it . a = { F where F is Filter of L : ( F in F_primeSet L & a in F ) } );
existence
ex b1 being Function st
for a being Element of L holds
( dom b1 = the carrier of L & b1 . a = { F where F is Filter of L : ( F in F_primeSet L & a in F ) } )
proof
deffunc H1( set ) -> set = { F where F is Filter of L : ( F in F_primeSet L & $1 in F ) } ;
consider f being Function such that
A1: ( dom f = the carrier of L & ( for x being set st x in the carrier of L holds
f . x = H1(x) ) ) from FUNCT_1:sch_3();
take f ; ::_thesis: for a being Element of L holds
( dom f = the carrier of L & f . a = { F where F is Filter of L : ( F in F_primeSet L & a in F ) } )
thus for a being Element of L holds
( dom f = the carrier of L & f . a = { F where F is Filter of L : ( F in F_primeSet L & a in F ) } ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function st ( for a being Element of L holds
( dom b1 = the carrier of L & b1 . a = { F where F is Filter of L : ( F in F_primeSet L & a in F ) } ) ) & ( for a being Element of L holds
( dom b2 = the carrier of L & b2 . a = { F where F is Filter of L : ( F in F_primeSet L & a in F ) } ) ) holds
b1 = b2
proof
let f1, f2 be Function; ::_thesis: ( ( for a being Element of L holds
( dom f1 = the carrier of L & f1 . a = { F where F is Filter of L : ( F in F_primeSet L & a in F ) } ) ) & ( for a being Element of L holds
( dom f2 = the carrier of L & f2 . a = { F where F is Filter of L : ( F in F_primeSet L & a in F ) } ) ) implies f1 = f2 )
assume that
A2: for a being Element of L holds
( dom f1 = the carrier of L & f1 . a = { F where F is Filter of L : ( F in F_primeSet L & a in F ) } ) and
A3: for a being Element of L holds
( dom f2 = the carrier of L & f2 . a = { F where F is Filter of L : ( F in F_primeSet L & a in F ) } ) ; ::_thesis: f1 = f2
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_L_holds_
f1_._x_=_f2_._x
let x be set ; ::_thesis: ( x in the carrier of L implies f1 . x = f2 . x )
assume x in the carrier of L ; ::_thesis: f1 . x = f2 . x
then reconsider a = x as Element of L ;
thus f1 . x = { F where F is Filter of L : ( F in F_primeSet L & a in F ) } by A2
.= f2 . x by A3 ; ::_thesis: verum
end;
hence f1 = f2 by A2, A3, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines StoneH OPENLATT:def_6_:_
for L being D_Lattice
for b2 being Function holds
( b2 = StoneH L iff for a being Element of L holds
( dom b2 = the carrier of L & b2 . a = { F where F is Filter of L : ( F in F_primeSet L & a in F ) } ) );
theorem Th11: :: OPENLATT:11
for L being D_Lattice
for F being Filter of L
for a being Element of L holds
( F in (StoneH L) . a iff ( F in F_primeSet L & a in F ) )
proof
let L be D_Lattice; ::_thesis: for F being Filter of L
for a being Element of L holds
( F in (StoneH L) . a iff ( F in F_primeSet L & a in F ) )
let F be Filter of L; ::_thesis: for a being Element of L holds
( F in (StoneH L) . a iff ( F in F_primeSet L & a in F ) )
let a be Element of L; ::_thesis: ( F in (StoneH L) . a iff ( F in F_primeSet L & a in F ) )
(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 ( F in (StoneH L) . a iff ( F in F_primeSet L & a in F ) ) ; ::_thesis: verum
end;
theorem Th12: :: OPENLATT:12
for L being D_Lattice
for a being Element of L
for x being set holds
( x in (StoneH L) . a iff ex F being Filter of L st
( F = x & F <> the carrier of L & F is prime & a in F ) )
proof
let L be D_Lattice; ::_thesis: for a being Element of L
for x being set holds
( x in (StoneH L) . a iff ex F being Filter of L st
( F = x & F <> the carrier of L & F is prime & a in F ) )
let a be Element of L; ::_thesis: for x being set holds
( x in (StoneH L) . a iff ex F being Filter of L st
( F = x & F <> the carrier of L & F is prime & a in F ) )
let x be set ; ::_thesis: ( x in (StoneH L) . a iff ex F being Filter of L st
( F = x & F <> the carrier of L & F is prime & a in F ) )
A1: (StoneH L) . a = { F where F is Filter of L : ( F in F_primeSet L & a in F ) } by Def6;
hereby ::_thesis: ( ex F being Filter of L st
( F = x & F <> the carrier of L & F is prime & a in F ) implies x in (StoneH L) . a )
assume x in (StoneH L) . a ; ::_thesis: ex F being Filter of L st
( F = x & F <> the carrier of L & F is prime & a in F )
then consider F being Filter of L such that
A2: x = F and
A3: F in F_primeSet L and
A4: a in F by A1;
A5: F is prime by A3, Th10;
F <> the carrier of L by A3, Th10;
hence ex F being Filter of L st
( F = x & F <> the carrier of L & F is prime & a in F ) by A2, A4, A5; ::_thesis: verum
end;
given F being Filter of L such that A6: F = x and
A7: F <> the carrier of L and
A8: F is prime and
A9: a in F ; ::_thesis: x in (StoneH L) . a
F in F_primeSet L by A7, A8;
hence x in (StoneH L) . a by A1, A6, A9; ::_thesis: verum
end;
definition
let L be D_Lattice;
func StoneS L -> set equals :: OPENLATT:def 7
rng (StoneH L);
coherence
rng (StoneH L) is set ;
end;
:: deftheorem defines StoneS OPENLATT:def_7_:_
for L being D_Lattice holds StoneS L = rng (StoneH L);
registration
let L be D_Lattice;
cluster StoneS L -> non empty ;
coherence
not StoneS L is empty
proof
dom (StoneH L) = the carrier of L by Def6;
hence not StoneS L is empty by RELAT_1:42; ::_thesis: verum
end;
end;
theorem Th13: :: OPENLATT:13
for L being D_Lattice
for x being set holds
( x in StoneS L iff ex a being Element of L st x = (StoneH L) . a )
proof
let L be D_Lattice; ::_thesis: for x being set holds
( x in StoneS L iff ex a being Element of L st x = (StoneH L) . a )
let x be set ; ::_thesis: ( x in StoneS L iff ex a being Element of L st x = (StoneH L) . a )
hereby ::_thesis: ( ex a being Element of L st x = (StoneH L) . a implies x in StoneS L )
assume x in StoneS L ; ::_thesis: ex y being Element of L st x = (StoneH L) . y
then consider y being set such that
A1: y in dom (StoneH L) and
A2: x = (StoneH L) . y by FUNCT_1:def_3;
reconsider y = y as Element of L by A1, Def6;
take y = y; ::_thesis: x = (StoneH L) . y
thus x = (StoneH L) . y by A2; ::_thesis: verum
end;
given b being Element of L such that A3: x = (StoneH L) . b ; ::_thesis: x in StoneS L
b in the carrier of L ;
then b in dom (StoneH L) by Def6;
hence x in StoneS L by A3, FUNCT_1:def_3; ::_thesis: verum
end;
theorem Th14: :: OPENLATT:14
for L being D_Lattice
for a, b being Element of L holds (StoneH L) . (a "\/" b) = ((StoneH L) . a) \/ ((StoneH L) . b)
proof
let L be D_Lattice; ::_thesis: for a, b being Element of L holds (StoneH L) . (a "\/" b) = ((StoneH L) . a) \/ ((StoneH L) . b)
let a, b be Element of L; ::_thesis: (StoneH L) . (a "\/" b) = ((StoneH L) . a) \/ ((StoneH L) . b)
set c = a "\/" b;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: ((StoneH L) . a) \/ ((StoneH L) . b) c= (StoneH L) . (a "\/" b)
set c = a "\/" b;
let x be set ; ::_thesis: ( x in (StoneH L) . (a "\/" b) implies x in ((StoneH L) . a) \/ ((StoneH L) . b) )
assume x in (StoneH L) . (a "\/" b) ; ::_thesis: x in ((StoneH L) . a) \/ ((StoneH L) . b)
then consider F being Filter of L such that
A1: x = F and
A2: F <> the carrier of L and
A3: F is prime and
A4: a "\/" b in F by Th12;
( a in F or b in F ) by A3, A4, FILTER_0:def_5;
then ( F in (StoneH L) . a or F in (StoneH L) . b ) by A2, A3, Th12;
hence x in ((StoneH L) . a) \/ ((StoneH L) . b) by A1, XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((StoneH L) . a) \/ ((StoneH L) . b) or x in (StoneH L) . (a "\/" b) )
assume x in ((StoneH L) . a) \/ ((StoneH L) . b) ; ::_thesis: x in (StoneH L) . (a "\/" b)
then ( x in (StoneH L) . a or x in (StoneH L) . b ) by XBOOLE_0:def_3;
then ( ex F being Filter of L st
( x = F & F <> the carrier of L & F is prime & a in F ) or ex F being Filter of L st
( x = F & F <> the carrier of L & F is prime & b in F ) ) by Th12;
then consider F being Filter of L such that
A5: x = F and
A6: F <> the carrier of L and
A7: F is prime and
A8: ( a in F or b in F ) ;
a "\/" b in F by A7, A8, FILTER_0:def_5;
hence x in (StoneH L) . (a "\/" b) by A5, A6, A7, Th12; ::_thesis: verum
end;
theorem Th15: :: OPENLATT:15
for L being D_Lattice
for a, b being Element of L holds (StoneH L) . (a "/\" b) = ((StoneH L) . a) /\ ((StoneH L) . b)
proof
let L be D_Lattice; ::_thesis: for a, b being Element of L holds (StoneH L) . (a "/\" b) = ((StoneH L) . a) /\ ((StoneH L) . b)
let a, b be Element of L; ::_thesis: (StoneH L) . (a "/\" b) = ((StoneH L) . a) /\ ((StoneH L) . b)
set c = a "/\" b;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: ((StoneH L) . a) /\ ((StoneH L) . b) c= (StoneH L) . (a "/\" b)
set c = a "/\" b;
let x be set ; ::_thesis: ( x in (StoneH L) . (a "/\" b) implies x in ((StoneH L) . a) /\ ((StoneH L) . b) )
assume x in (StoneH L) . (a "/\" b) ; ::_thesis: x in ((StoneH L) . a) /\ ((StoneH L) . b)
then consider F being Filter of L such that
A1: x = F and
A2: F <> the carrier of L and
A3: F is prime and
A4: a "/\" b in F by Th12;
b in F by A4, FILTER_0:8;
then A5: F in (StoneH L) . b by A2, A3, Th12;
a in F by A4, FILTER_0:8;
then F in (StoneH L) . a by A2, A3, Th12;
hence x in ((StoneH L) . a) /\ ((StoneH L) . b) by A1, A5, XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((StoneH L) . a) /\ ((StoneH L) . b) or x in (StoneH L) . (a "/\" b) )
assume A6: x in ((StoneH L) . a) /\ ((StoneH L) . b) ; ::_thesis: x in (StoneH L) . (a "/\" b)
then x in (StoneH L) . b by XBOOLE_0:def_4;
then A7: ex F being Filter of L st
( x = F & F <> the carrier of L & F is prime & b in F ) by Th12;
x in (StoneH L) . a by A6, XBOOLE_0:def_4;
then ex F being Filter of L st
( x = F & F <> the carrier of L & F is prime & a in F ) by Th12;
then consider F being Filter of L such that
A8: x = F and
A9: F <> the carrier of L and
A10: F is prime and
A11: a in F and
A12: b in F by A7;
a "/\" b in F by A11, A12, FILTER_0:8;
hence x in (StoneH L) . (a "/\" b) by A8, A9, A10, Th12; ::_thesis: verum
end;
definition
let L be D_Lattice;
let a be Element of L;
func SF_have a -> Subset-Family of L equals :: OPENLATT:def 8
{ F where F is Filter of L : a in F } ;
coherence
{ F where F is Filter of L : a in F } is Subset-Family of L
proof
set A = { F where F is Filter of L : a in F } ;
{ F where F is Filter of L : a in F } c= bool the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { F where F is Filter of L : a in F } or x in bool the carrier of L )
assume x in { F where F is Filter of L : a in F } ; ::_thesis: x in bool the carrier of L
then ex F being Filter of L st
( x = F & a in F ) ;
hence x in bool the carrier of L ; ::_thesis: verum
end;
hence { F where F is Filter of L : a in F } is Subset-Family of L ; ::_thesis: verum
end;
end;
:: deftheorem defines SF_have OPENLATT:def_8_:_
for L being D_Lattice
for a being Element of L holds SF_have a = { F where F is Filter of L : a in F } ;
registration
let L be D_Lattice;
let a be Element of L;
cluster SF_have a -> non empty ;
coherence
not SF_have a is empty
proof
a in <.a.) ;
then <.a.) in { F where F is Filter of L : a in F } ;
hence not SF_have a is empty ; ::_thesis: verum
end;
end;
theorem Th16: :: OPENLATT:16
for L being D_Lattice
for a being Element of L
for x being set holds
( x in SF_have a iff ( x is Filter of L & a in x ) )
proof
let L be D_Lattice; ::_thesis: for a being Element of L
for x being set holds
( x in SF_have a iff ( x is Filter of L & a in x ) )
let a be Element of L; ::_thesis: for x being set holds
( x in SF_have a iff ( x is Filter of L & a in x ) )
let x be set ; ::_thesis: ( x in SF_have a iff ( x is Filter of L & a in x ) )
( x in SF_have a iff ex F being Filter of L st
( F = x & a in F ) ) ;
hence ( x in SF_have a iff ( x is Filter of L & a in x ) ) ; ::_thesis: verum
end;
Lm1: for L being D_Lattice
for F being Filter of L
for b, a being Element of L holds
( F in (SF_have b) \ (SF_have a) iff ( b in F & not a in F ) )
proof
let L be D_Lattice; ::_thesis: for F being Filter of L
for b, a being Element of L holds
( F in (SF_have b) \ (SF_have a) iff ( b in F & not a in F ) )
let F be Filter of L; ::_thesis: for b, a being Element of L holds
( F in (SF_have b) \ (SF_have a) iff ( b in F & not a in F ) )
let b, a be Element of L; ::_thesis: ( F in (SF_have b) \ (SF_have a) iff ( b in F & not a in F ) )
( F in (SF_have b) \ (SF_have a) iff ( F in SF_have b & not F in SF_have a ) ) by XBOOLE_0:def_5;
hence ( F in (SF_have b) \ (SF_have a) iff ( b in F & not a in F ) ) by Th16; ::_thesis: verum
end;
theorem Th17: :: OPENLATT:17
for L being D_Lattice
for b, a being Element of L
for x being set st x in (SF_have b) \ (SF_have a) holds
( x is Filter of L & b in x & not a in x )
proof
let L be D_Lattice; ::_thesis: for b, a being Element of L
for x being set st x in (SF_have b) \ (SF_have a) holds
( x is Filter of L & b in x & not a in x )
let b, a be Element of L; ::_thesis: for x being set st x in (SF_have b) \ (SF_have a) holds
( x is Filter of L & b in x & not a in x )
let x be set ; ::_thesis: ( x in (SF_have b) \ (SF_have a) implies ( x is Filter of L & b in x & not a in x ) )
assume A1: x in (SF_have b) \ (SF_have a) ; ::_thesis: ( x is Filter of L & b in x & not a in x )
then A2: not x in SF_have a by XBOOLE_0:def_5;
A3: x in SF_have b by A1, XBOOLE_0:def_5;
then x is Filter of L by Th16;
hence ( x is Filter of L & b in x & not a in x ) by A3, A2, Th16; ::_thesis: verum
end;
theorem Th18: :: OPENLATT:18
for L being D_Lattice
for b, a being Element of L
for Z being set st Z <> {} & Z c= (SF_have b) \ (SF_have a) & Z is c=-linear holds
ex Y being set st
( Y in (SF_have b) \ (SF_have a) & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
proof
let L be D_Lattice; ::_thesis: for b, a being Element of L
for Z being set st Z <> {} & Z c= (SF_have b) \ (SF_have a) & Z is c=-linear holds
ex Y being set st
( Y in (SF_have b) \ (SF_have a) & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
let b, a be Element of L; ::_thesis: for Z being set st Z <> {} & Z c= (SF_have b) \ (SF_have a) & Z is c=-linear holds
ex Y being set st
( Y in (SF_have b) \ (SF_have a) & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
let Z be set ; ::_thesis: ( Z <> {} & Z c= (SF_have b) \ (SF_have a) & Z is c=-linear implies ex Y being set st
( Y in (SF_have b) \ (SF_have a) & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) )
assume that
A1: Z <> {} and
A2: Z c= (SF_have b) \ (SF_have a) and
A3: Z is c=-linear ; ::_thesis: ex Y being set st
( Y in (SF_have b) \ (SF_have a) & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
reconsider Z = Z as Subset-Family of L by A2, XBOOLE_1:1;
take Y = union Z; ::_thesis: ( Y in (SF_have b) \ (SF_have a) & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
Y in (SF_have b) \ (SF_have a)
proof
set X = the Element of Z;
A4: not a in Y
proof
assume a in Y ; ::_thesis: contradiction
then ex X being set st
( a in X & X in Z ) by TARSKI:def_4;
hence contradiction by A2, Th17; ::_thesis: verum
end;
the Element of Z in (SF_have b) \ (SF_have a) by A1, A2, TARSKI:def_3;
then A5: b in the Element of Z by Th17;
then A6: b in Y by A1, TARSKI:def_4;
reconsider Y = Y as non empty Subset of L by A1, A5, TARSKI:def_4;
now__::_thesis:_for_p,_q_being_Element_of_L_holds_
(_(_p_in_Y_&_q_in_Y_implies_p_"/\"_q_in_Y_)_&_(_p_"/\"_q_in_Y_implies_(_p_in_Y_&_q_in_Y_)_)_)
let p, q be Element of L; ::_thesis: ( ( p in Y & q in Y implies p "/\" q in Y ) & ( p "/\" q in Y implies ( p in Y & q in Y ) ) )
thus ( p in Y & q in Y implies p "/\" q in Y ) ::_thesis: ( p "/\" q in Y implies ( p in Y & q in Y ) )
proof
assume p in Y ; ::_thesis: ( not q in Y or p "/\" q in Y )
then consider X1 being set such that
A7: p in X1 and
A8: X1 in Z by TARSKI:def_4;
A9: X1 is Filter of L by A2, A8, Th17;
assume q in Y ; ::_thesis: p "/\" q in Y
then consider X2 being set such that
A10: q in X2 and
A11: X2 in Z by TARSKI:def_4;
X1,X2 are_c=-comparable by A3, A8, A11, ORDINAL1:def_8;
then A12: ( X1 c= X2 or X2 c= X1 ) by XBOOLE_0:def_9;
X2 is Filter of L by A2, A11, Th17;
then ( p "/\" q in X1 or p "/\" q in X2 ) by A7, A10, A9, A12, FILTER_0:8;
hence p "/\" q in Y by A8, A11, TARSKI:def_4; ::_thesis: verum
end;
assume p "/\" q in Y ; ::_thesis: ( p in Y & q in Y )
then consider X1 being set such that
A13: p "/\" q in X1 and
A14: X1 in Z by TARSKI:def_4;
A15: X1 is Filter of L by A2, A14, Th17;
then A16: q in X1 by A13, FILTER_0:8;
p in X1 by A13, A15, FILTER_0:8;
hence ( p in Y & q in Y ) by A14, A16, TARSKI:def_4; ::_thesis: verum
end;
then Y is Filter of L by FILTER_0:8;
hence Y in (SF_have b) \ (SF_have a) by A4, A6, Lm1; ::_thesis: verum
end;
hence ( Y in (SF_have b) \ (SF_have a) & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) by ZFMISC_1:74; ::_thesis: verum
end;
theorem Th19: :: OPENLATT:19
for L being D_Lattice
for b, a being Element of L st not b [= a holds
<.b.) in (SF_have b) \ (SF_have a)
proof
let L be D_Lattice; ::_thesis: for b, a being Element of L st not b [= a holds
<.b.) in (SF_have b) \ (SF_have a)
let b, a be Element of L; ::_thesis: ( not b [= a implies <.b.) in (SF_have b) \ (SF_have a) )
assume not b [= a ; ::_thesis: <.b.) in (SF_have b) \ (SF_have a)
then not a in <.b.) by FILTER_0:15;
then A1: not <.b.) in SF_have a by Th16;
b in <.b.) ;
then <.b.) in SF_have b ;
hence <.b.) in (SF_have b) \ (SF_have a) by A1, XBOOLE_0:def_5; ::_thesis: verum
end;
theorem Th20: :: OPENLATT:20
for L being D_Lattice
for b, a being Element of L st not b [= a holds
ex F being Filter of L st
( F in F_primeSet L & not a in F & b in F )
proof
let L be D_Lattice; ::_thesis: for b, a being Element of L st not b [= a holds
ex F being Filter of L st
( F in F_primeSet L & not a in F & b in F )
let b, a be Element of L; ::_thesis: ( not b [= a implies ex F being Filter of L st
( F in F_primeSet L & not a in F & b in F ) )
set A = (SF_have b) \ (SF_have a);
assume not b [= a ; ::_thesis: ex F being Filter of L st
( F in F_primeSet L & not a in F & b in F )
then A1: (SF_have b) \ (SF_have a) <> {} by Th19;
for Z being set st Z <> {} & Z c= (SF_have b) \ (SF_have a) & Z is c=-linear holds
ex Y being set st
( Y in (SF_have b) \ (SF_have a) & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) by Th18;
then consider Y being set such that
A2: Y in (SF_have b) \ (SF_have a) and
A3: for Z being set st Z in (SF_have b) \ (SF_have a) & Z <> Y holds
not Y c= Z by A1, LATTICE4:1;
reconsider Y = Y as Filter of L by A2, Th17;
A4: b in Y by A2, Th17;
A5: not a in Y by A2, Th17;
A6: Y is prime
proof
let a1, a2 be Element of L; :: according to FILTER_0:def_5 ::_thesis: ( ( not a1 "\/" a2 in Y or a1 in Y or a2 in Y ) & ( ( not a1 in Y & not a2 in Y ) or a1 "\/" a2 in Y ) )
thus ( not a1 "\/" a2 in Y or a1 in Y or a2 in Y ) ::_thesis: ( ( not a1 in Y & not a2 in Y ) or a1 "\/" a2 in Y )
proof
set F2 = <.(<.a2.) \/ Y).);
set F1 = <.(<.a1.) \/ Y).);
assume that
A7: a1 "\/" a2 in Y and
A8: not a1 in Y and
A9: not a2 in Y ; ::_thesis: contradiction
A10: <.a1.) c= <.(<.a1.) \/ Y).) by LATTICE4:2;
a1 in <.a1.) ;
then A11: a1 in <.(<.a1.) \/ Y).) by A10;
A12: Y c= <.(<.a1.) \/ Y).) by LATTICE4:2;
A13: <.a2.) c= <.(<.a2.) \/ Y).) by LATTICE4:2;
a2 in <.a2.) ;
then A14: a2 in <.(<.a2.) \/ Y).) by A13;
A15: Y c= <.(<.a2.) \/ Y).) by LATTICE4:2;
( not a in <.(<.a1.) \/ Y).) or not a in <.(<.a2.) \/ Y).) )
proof
assume that
A16: a in <.(<.a1.) \/ Y).) and
A17: a in <.(<.a2.) \/ Y).) ; ::_thesis: contradiction
consider c1 being Element of L such that
A18: c1 in Y and
A19: a1 "/\" c1 [= a by A16, LATTICE4:3;
consider c2 being Element of L such that
A20: c2 in Y and
A21: a2 "/\" c2 [= a by A17, LATTICE4:3;
set c = c1 "/\" c2;
a2 "/\" (c1 "/\" c2) [= a2 "/\" c2 by LATTICES:6, LATTICES:9;
then A22: a2 "/\" (c1 "/\" c2) [= a by A21, LATTICES:7;
a1 "/\" (c1 "/\" c2) [= a1 "/\" c1 by LATTICES:6, LATTICES:9;
then a1 "/\" (c1 "/\" c2) [= a by A19, LATTICES:7;
then (a1 "/\" (c1 "/\" c2)) "\/" (a2 "/\" (c1 "/\" c2)) [= a by A22, FILTER_0:6;
then A23: (a1 "\/" a2) "/\" (c1 "/\" c2) [= a by LATTICES:def_11;
c1 "/\" c2 in Y by A18, A20, FILTER_0:8;
then (a1 "\/" a2) "/\" (c1 "/\" c2) in Y by A7, FILTER_0:8;
hence contradiction by A5, A23, FILTER_0:9; ::_thesis: verum
end;
then ( <.(<.a1.) \/ Y).) in (SF_have b) \ (SF_have a) or <.(<.a2.) \/ Y).) in (SF_have b) \ (SF_have a) ) by A4, A12, A15, Lm1;
hence contradiction by A3, A8, A9, A11, A14, A12, A15; ::_thesis: verum
end;
thus ( ( not a1 in Y & not a2 in Y ) or a1 "\/" a2 in Y ) by FILTER_0:10; ::_thesis: verum
end;
Y <> the carrier of L by A2, Th17;
then Y in F_primeSet L by A6;
hence ex F being Filter of L st
( F in F_primeSet L & not a in F & b in F ) by A5, A4; ::_thesis: verum
end;
theorem Th21: :: OPENLATT:21
for L being D_Lattice
for a, b being Element of L st a <> b holds
ex F being Filter of L st F in F_primeSet L
proof
let L be D_Lattice; ::_thesis: for a, b being Element of L st a <> b holds
ex F being Filter of L st F in F_primeSet L
let a, b be Element of L; ::_thesis: ( a <> b implies ex F being Filter of L st F in F_primeSet L )
assume a <> b ; ::_thesis: ex F being Filter of L st F in F_primeSet L
then ( not a [= b or not b [= a ) by LATTICES:8;
then ( ex F being Filter of L st
( F in F_primeSet L & not b in F & a in F ) or ex F being Filter of L st
( F in F_primeSet L & not a in F & b in F ) ) by Th20;
hence ex F being Filter of L st F in F_primeSet L ; ::_thesis: verum
end;
theorem Th22: :: OPENLATT:22
for L being D_Lattice
for a, b being Element of L st a <> b holds
(StoneH L) . a <> (StoneH L) . b
proof
let L be D_Lattice; ::_thesis: for a, b being Element of L st a <> b holds
(StoneH L) . a <> (StoneH L) . b
let a, b be Element of L; ::_thesis: ( a <> b implies (StoneH L) . a <> (StoneH L) . b )
assume a <> b ; ::_thesis: (StoneH L) . a <> (StoneH L) . b
then ( not a [= b or not b [= a ) by LATTICES:8;
then ( ex F being Filter of L st
( F in F_primeSet L & not b in F & a in F ) or ex F being Filter of L st
( F in F_primeSet L & not a in F & b in F ) ) by Th20;
then consider F being Filter of L such that
A1: F in F_primeSet L and
A2: ( ( 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, A2, Th11;
hence (StoneH L) . a <> (StoneH L) . b ; ::_thesis: verum
end;
registration
let L be D_Lattice;
cluster StoneH L -> one-to-one ;
coherence
StoneH L is one-to-one
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom (StoneH L) or not x2 in dom (StoneH L) or not (StoneH L) . x1 = (StoneH L) . x2 or x1 = x2 )
assume that
A1: x1 in dom (StoneH L) and
A2: x2 in dom (StoneH L) and
A3: (StoneH L) . x1 = (StoneH L) . x2 ; ::_thesis: x1 = x2
reconsider a1 = x1, a2 = x2 as Element of L by A1, A2, Def6;
a1 = a2 by A3, Th22;
hence x1 = x2 ; ::_thesis: verum
end;
end;
definition
let L be D_Lattice;
let A, B be Element of StoneS L;
:: original: \/
redefine funcA \/ B -> Element of StoneS L;
coherence
A \/ B is Element of StoneS L
proof
consider b being Element of L such that
A1: B = (StoneH L) . b by Th13;
consider a being Element of L such that
A2: A = (StoneH L) . a by Th13;
A \/ B = (StoneH L) . (a "\/" b) by A2, A1, Th14;
hence A \/ B is Element of StoneS L by Th13; ::_thesis: verum
end;
:: original: /\
redefine funcA /\ B -> Element of StoneS L;
coherence
A /\ B is Element of StoneS L
proof
consider b being Element of L such that
A3: B = (StoneH L) . b by Th13;
consider a being Element of L such that
A4: A = (StoneH L) . a by Th13;
A /\ B = (StoneH L) . (a "/\" b) by A4, A3, Th15;
hence A /\ B is Element of StoneS L by Th13; ::_thesis: verum
end;
end;
definition
let L be D_Lattice;
func Set_Union L -> BinOp of (StoneS L) means :Def9: :: OPENLATT:def 9
for A, B being Element of StoneS L holds it . (A,B) = A \/ B;
existence
ex b1 being BinOp of (StoneS L) st
for A, B being Element of StoneS L holds b1 . (A,B) = A \/ B
proof
deffunc H1( Element of StoneS L, 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) = H1(P,Q) from BINOP_1:sch_4(); ::_thesis: verum
end;
uniqueness
for b1, b2 being BinOp of (StoneS L) st ( for A, B being Element of StoneS L holds b1 . (A,B) = A \/ B ) & ( for A, B being Element of StoneS L holds b2 . (A,B) = A \/ B ) holds
b1 = b2
proof
set A = StoneS L;
deffunc H1( Element of StoneS L, Element of StoneS L) -> Element of StoneS L = $1 \/ $2;
thus for o1, o2 being BinOp of (StoneS L) st ( for a, b being Element of StoneS L holds o1 . (a,b) = H1(a,b) ) & ( for a, b being Element of StoneS L holds o2 . (a,b) = H1(a,b) ) holds
o1 = o2 from BINOP_2:sch_2(); ::_thesis: verum
end;
func Set_Meet L -> BinOp of (StoneS L) means :Def10: :: OPENLATT:def 10
for A, B being Element of StoneS L holds it . (A,B) = A /\ B;
existence
ex b1 being BinOp of (StoneS L) st
for A, B being Element of StoneS L holds b1 . (A,B) = A /\ B
proof
deffunc H1( Element of StoneS L, 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) = H1(P,Q) from BINOP_1:sch_4(); ::_thesis: verum
end;
uniqueness
for b1, b2 being BinOp of (StoneS L) st ( for A, B being Element of StoneS L holds b1 . (A,B) = A /\ B ) & ( for A, B being Element of StoneS L holds b2 . (A,B) = A /\ B ) holds
b1 = b2
proof
set A = StoneS L;
deffunc H1( Element of StoneS L, Element of StoneS L) -> Element of StoneS L = $1 /\ $2;
thus for o1, o2 being BinOp of (StoneS L) st ( for a, b being Element of StoneS L holds o1 . (a,b) = H1(a,b) ) & ( for a, b being Element of StoneS L holds o2 . (a,b) = H1(a,b) ) holds
o1 = o2 from BINOP_2:sch_2(); ::_thesis: verum
end;
end;
:: deftheorem Def9 defines Set_Union OPENLATT:def_9_:_
for L being D_Lattice
for b2 being BinOp of (StoneS L) holds
( b2 = Set_Union L iff for A, B being Element of StoneS L holds b2 . (A,B) = A \/ B );
:: deftheorem Def10 defines Set_Meet OPENLATT:def_10_:_
for L being D_Lattice
for b2 being BinOp of (StoneS L) holds
( b2 = Set_Meet L iff for A, B being Element of StoneS L holds b2 . (A,B) = A /\ B );
theorem Th23: :: OPENLATT:23
for L being D_Lattice holds LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is Lattice
proof
let L be D_Lattice; ::_thesis: LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is Lattice
set SL = LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #);
A1: now__::_thesis:_for_p,_q_being_Element_of_LattStr(#_(StoneS_L),(Set_Union_L),(Set_Meet_L)_#)_holds_p_"\/"_q_=_q_"\/"_p
let p, q be Element of LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #); ::_thesis: p "\/" q = q "\/" p
thus p "\/" q = q \/ p by Def9
.= q "\/" p by Def9 ; ::_thesis: verum
end;
A2: now__::_thesis:_for_p,_q_being_Element_of_LattStr(#_(StoneS_L),(Set_Union_L),(Set_Meet_L)_#)_holds_(p_"/\"_q)_"\/"_q_=_q
let p, q be Element of LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #); ::_thesis: (p "/\" q) "\/" q = q
thus (p "/\" q) "\/" q = (p "/\" q) \/ q by Def9
.= (p /\ q) \/ q by Def10
.= q by XBOOLE_1:22 ; ::_thesis: verum
end;
A3: now__::_thesis:_for_p,_q_being_Element_of_LattStr(#_(StoneS_L),(Set_Union_L),(Set_Meet_L)_#)_holds_p_"/\"_(p_"\/"_q)_=_p
let p, q be Element of LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #); ::_thesis: p "/\" (p "\/" q) = p
thus p "/\" (p "\/" q) = p /\ (p "\/" q) by Def10
.= p /\ (p \/ q) by Def9
.= p by XBOOLE_1:21 ; ::_thesis: verum
end;
A4: now__::_thesis:_for_p,_q,_r_being_Element_of_LattStr(#_(StoneS_L),(Set_Union_L),(Set_Meet_L)_#)_holds_p_"/\"_(q_"/\"_r)_=_(p_"/\"_q)_"/\"_r
let p, q, r be Element of LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #); ::_thesis: p "/\" (q "/\" r) = (p "/\" q) "/\" r
thus p "/\" (q "/\" r) = p /\ (q "/\" r) by Def10
.= p /\ (q /\ r) by Def10
.= (p /\ q) /\ r by XBOOLE_1:16
.= (p "/\" q) /\ r by Def10
.= (p "/\" q) "/\" r by Def10 ; ::_thesis: verum
end;
A5: now__::_thesis:_for_p,_q_being_Element_of_LattStr(#_(StoneS_L),(Set_Union_L),(Set_Meet_L)_#)_holds_p_"/\"_q_=_q_"/\"_p
let p, q be Element of LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #); ::_thesis: p "/\" q = q "/\" p
thus p "/\" q = q /\ p by Def10
.= q "/\" p by Def10 ; ::_thesis: verum
end;
now__::_thesis:_for_p,_q,_r_being_Element_of_LattStr(#_(StoneS_L),(Set_Union_L),(Set_Meet_L)_#)_holds_p_"\/"_(q_"\/"_r)_=_(p_"\/"_q)_"\/"_r
let p, q, r be Element of LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #); ::_thesis: p "\/" (q "\/" r) = (p "\/" q) "\/" r
thus p "\/" (q "\/" r) = p \/ (q "\/" r) by Def9
.= p \/ (q \/ r) by Def9
.= (p \/ q) \/ r by XBOOLE_1:4
.= (p "\/" q) \/ r by Def9
.= (p "\/" q) "\/" r by Def9 ; ::_thesis: verum
end;
then ( LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is join-commutative & LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is join-associative & LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is meet-absorbing & LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is meet-commutative & LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is meet-associative & LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is join-absorbing ) by A1, A2, A5, A4, A3, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9;
hence LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is Lattice ; ::_thesis: verum
end;
definition
let L be D_Lattice;
func StoneLatt L -> Lattice equals :: OPENLATT:def 11
LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #);
coherence
LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is Lattice by Th23;
end;
:: deftheorem defines StoneLatt OPENLATT:def_11_:_
for L being D_Lattice holds StoneLatt L = LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #);
theorem :: OPENLATT:24
for L being D_Lattice holds the carrier of (StoneLatt L) = StoneS L ;
theorem :: OPENLATT:25
for L being D_Lattice
for p, q being Element of (StoneLatt L) holds
( p "\/" q = p \/ q & p "/\" q = p /\ q ) by Def9, Def10;
theorem :: OPENLATT:26
for L being D_Lattice
for p, q being Element of (StoneLatt L) holds
( p [= q iff p c= q )
proof
let L be D_Lattice; ::_thesis: for p, q being Element of (StoneLatt L) holds
( p [= q iff p c= q )
let p, q be Element of (StoneLatt L); ::_thesis: ( p [= q iff p c= q )
A1: ( p [= q iff p "\/" q = q ) by LATTICES:def_3;
p "\/" q = p \/ q by Def9;
hence ( p [= q iff p c= q ) by A1, XBOOLE_1:7, XBOOLE_1:12; ::_thesis: verum
end;
definition
let L be D_Lattice;
:: original: StoneH
redefine func StoneH L -> Homomorphism of L, StoneLatt L;
coherence
StoneH L is Homomorphism of L, StoneLatt L
proof
dom (StoneH L) = the carrier of L by Def6;
then reconsider f = StoneH L as Function of the carrier of L, the carrier of (StoneLatt L) by FUNCT_2:1;
now__::_thesis:_for_a,_b_being_Element_of_L_holds_
(_f_._(a_"\/"_b)_=_(f_._a)_"\/"_(f_._b)_&_f_._(a_"/\"_b)_=_(f_._a)_"/\"_(f_._b)_)
let a, b be Element of L; ::_thesis: ( f . (a "\/" b) = (f . a) "\/" (f . b) & f . (a "/\" b) = (f . a) "/\" (f . b) )
thus f . (a "\/" b) = (f . a) \/ (f . b) by Th14
.= (f . a) "\/" (f . b) by Def9 ; ::_thesis: f . (a "/\" b) = (f . a) "/\" (f . b)
thus f . (a "/\" b) = (f . a) /\ (f . b) by Th15
.= (f . a) "/\" (f . b) by Def10 ; ::_thesis: verum
end;
hence StoneH L is Homomorphism of L, StoneLatt L by LATTICE4:def_1; ::_thesis: verum
end;
end;
registration
let L be D_Lattice;
cluster StoneH L -> bijective for Function of L,(StoneLatt L);
coherence
for b1 being Function of L,(StoneLatt L) st b1 = StoneH L holds
b1 is bijective
proof
now__::_thesis:_(_StoneH_L_is_one-to-one_&_StoneH_L_is_onto_)
thus StoneH L is one-to-one ; ::_thesis: StoneH L is onto
thus StoneH L is onto ::_thesis: verum
proof
thus rng (StoneH L) = the carrier of (StoneLatt L) ; :: according to FUNCT_2:def_3 ::_thesis: verum
end;
end;
hence for b1 being Function of L,(StoneLatt L) st b1 = StoneH L holds
b1 is bijective by FUNCT_2:def_4; ::_thesis: verum
end;
cluster StoneLatt L -> distributive ;
coherence
StoneLatt L is distributive
proof
StoneH L is onto by FUNCT_2:def_3;
hence StoneLatt L is distributive by LATTICE4:11; ::_thesis: verum
end;
end;
theorem :: OPENLATT:27
for L being D_Lattice holds L, StoneLatt L are_isomorphic
proof
let L be D_Lattice; ::_thesis: L, StoneLatt L are_isomorphic
take StoneH L ; :: according to LATTICE4:def_2 ::_thesis: StoneH L is bijective
thus StoneH L is bijective ; ::_thesis: verum
end;
registration
cluster non empty non trivial join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V90() Heyting implicative for LattStr ;
existence
not for b1 being H_Lattice holds b1 is trivial
proof
set T = the non empty TopSpace;
set OL = Open_setLatt the non empty TopSpace;
the carrier of the non empty TopSpace = Top (Open_setLatt the non empty TopSpace) by Th9;
then reconsider a = the carrier of the non empty TopSpace as Element of (Open_setLatt the non empty TopSpace) ;
{} = Bottom (Open_setLatt the non empty TopSpace) by Th8;
then reconsider b = {} as Element of (Open_setLatt the non empty TopSpace) ;
take Open_setLatt the non empty TopSpace ; ::_thesis: not Open_setLatt the non empty TopSpace is trivial
take a ; :: according to STRUCT_0:def_10 ::_thesis: not for b1 being Element of the carrier of (Open_setLatt the non empty TopSpace) holds a = b1
take b ; ::_thesis: not a = b
thus not a = b ; ::_thesis: verum
end;
end;
theorem Th28: :: OPENLATT:28
for H being non trivial H_Lattice holds (StoneH H) . (Top H) = F_primeSet H
proof
let H be non trivial H_Lattice; ::_thesis: (StoneH H) . (Top H) = F_primeSet H
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: F_primeSet H c= (StoneH H) . (Top H)
let x be set ; ::_thesis: ( x in (StoneH H) . (Top H) implies x in F_primeSet H )
assume x in (StoneH H) . (Top H) ; ::_thesis: x in F_primeSet H
then ex F being Filter of H st
( F = x & F <> the carrier of H & F is prime & Top H in F ) by Th12;
hence x in F_primeSet H ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F_primeSet H or x in (StoneH H) . (Top H) )
assume x in F_primeSet H ; ::_thesis: x in (StoneH H) . (Top H)
then consider F being Filter of H such that
A1: F = x and
A2: F <> the carrier of H and
A3: F is prime ;
Top H in F by FILTER_0:11;
hence x in (StoneH H) . (Top H) by A1, A2, A3, Th12; ::_thesis: verum
end;
theorem Th29: :: OPENLATT:29
for H being non trivial H_Lattice holds (StoneH H) . (Bottom H) = {}
proof
let H be non trivial H_Lattice; ::_thesis: (StoneH H) . (Bottom H) = {}
set x = the Element of (StoneH H) . (Bottom H);
assume (StoneH H) . (Bottom H) <> {} ; ::_thesis: contradiction
then ex F being Filter of H st
( F = the Element of (StoneH H) . (Bottom H) & F <> the carrier of H & F is prime & Bottom H in F ) by Th12;
hence contradiction by FILTER_0:26; ::_thesis: verum
end;
theorem Th30: :: OPENLATT:30
for H being non trivial H_Lattice holds StoneS H c= bool (F_primeSet H)
proof
let H be non trivial H_Lattice; ::_thesis: StoneS H c= bool (F_primeSet H)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in StoneS H or x in bool (F_primeSet H) )
assume x in StoneS H ; ::_thesis: x in bool (F_primeSet H)
then consider p9 being Element of H such that
A1: x = (StoneH H) . p9 by Th13;
A2: x = { F where F is Filter of H : ( F in F_primeSet H & p9 in F ) } by A1, Def6;
x c= F_primeSet H
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in x or y in F_primeSet H )
assume y in x ; ::_thesis: y in F_primeSet H
then ex F being Filter of H st
( y = F & F in F_primeSet H & p9 in F ) by A2;
hence y in F_primeSet H ; ::_thesis: verum
end;
hence x in bool (F_primeSet H) ; ::_thesis: verum
end;
registration
let H be non trivial H_Lattice;
cluster F_primeSet H -> non empty ;
coherence
not F_primeSet H is empty
proof
ex p9, q9 being Element of H st p9 <> q9 by STRUCT_0:def_10;
then ex F being Filter of H st F in F_primeSet H by Th21;
hence not F_primeSet H is empty ; ::_thesis: verum
end;
end;
definition
let H be non trivial H_Lattice;
func HTopSpace H -> strict TopStruct means :Def12: :: OPENLATT:def 12
( the carrier of it = F_primeSet H & the topology of it = { (union A) where A is Subset of (StoneS H) : verum } );
existence
ex b1 being strict TopStruct st
( the carrier of b1 = F_primeSet H & the topology of b1 = { (union A) where A is Subset of (StoneS H) : verum } )
proof
set FS = F_primeSet H;
set top = { (union A) where A is Subset of (StoneS H) : verum } ;
A1: StoneS H c= bool (F_primeSet H) by Th30;
{ (union A) where A is Subset of (StoneS H) : verum } c= bool (F_primeSet H)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (union A) where A is Subset of (StoneS H) : verum } or x in bool (F_primeSet H) )
assume x in { (union A) where A is Subset of (StoneS H) : verum } ; ::_thesis: x in bool (F_primeSet H)
then consider A being Subset of (StoneS H) such that
A2: x = union A ;
A c= bool (F_primeSet H) by A1, XBOOLE_1:1;
then x c= union (bool (F_primeSet H)) by A2, ZFMISC_1:77;
then x is Subset of (F_primeSet H) by ZFMISC_1:81;
hence x in bool (F_primeSet H) ; ::_thesis: verum
end;
then reconsider top = { (union A) where A is Subset of (StoneS H) : verum } as Subset-Family of (F_primeSet H) ;
take TopStruct(# (F_primeSet H),top #) ; ::_thesis: ( the carrier of TopStruct(# (F_primeSet H),top #) = F_primeSet H & the topology of TopStruct(# (F_primeSet H),top #) = { (union A) where A is Subset of (StoneS H) : verum } )
thus ( the carrier of TopStruct(# (F_primeSet H),top #) = F_primeSet H & the topology of TopStruct(# (F_primeSet H),top #) = { (union A) where A is Subset of (StoneS H) : verum } ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict TopStruct st the carrier of b1 = F_primeSet H & the topology of b1 = { (union A) where A is Subset of (StoneS H) : verum } & the carrier of b2 = F_primeSet H & the topology of b2 = { (union A) where A is Subset of (StoneS H) : verum } holds
b1 = b2 ;
end;
:: deftheorem Def12 defines HTopSpace OPENLATT:def_12_:_
for H being non trivial H_Lattice
for b2 being strict TopStruct holds
( b2 = HTopSpace H iff ( the carrier of b2 = F_primeSet H & the topology of b2 = { (union A) where A is Subset of (StoneS H) : verum } ) );
registration
let H be non trivial H_Lattice;
cluster HTopSpace H -> non empty strict TopSpace-like ;
coherence
( not HTopSpace H is empty & HTopSpace H is TopSpace-like )
proof
reconsider A1 = {((StoneH H) . (Top H))} as Subset of (StoneS H) ;
set TS = HTopSpace H;
A1: the topology of (HTopSpace H) = { (union A) where A is Subset of (StoneS H) : verum } by Def12;
A2: the carrier of (HTopSpace H) = F_primeSet H by Def12;
hence not HTopSpace H is empty ; ::_thesis: HTopSpace H is TopSpace-like
F_primeSet H = (StoneH H) . (Top H) by Th28;
then F_primeSet H = union A1 by ZFMISC_1:25;
hence the carrier of (HTopSpace H) in the topology of (HTopSpace H) by A2, A1; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of K19(K19( the carrier of (HTopSpace H))) holds
( not b1 c= the topology of (HTopSpace H) or union b1 in the topology of (HTopSpace H) ) ) & ( for b1, b2 being Element of K19( the carrier of (HTopSpace H)) holds
( not b1 in the topology of (HTopSpace H) or not b2 in the topology of (HTopSpace H) or b1 /\ b2 in the topology of (HTopSpace H) ) ) )
hereby ::_thesis: for b1, b2 being Element of K19( the carrier of (HTopSpace H)) holds
( not b1 in the topology of (HTopSpace H) or not b2 in the topology of (HTopSpace H) or b1 /\ b2 in the topology of (HTopSpace H) )
let a be Subset-Family of (HTopSpace H); ::_thesis: ( a c= the topology of (HTopSpace H) implies union a in the topology of (HTopSpace H) )
defpred S1[ set ] means union H in a;
set B = { A where A is Subset of (StoneS H) : S1[A] } ;
set X = { (union A) where A is Subset of (StoneS H) : A in { A where A is Subset of (StoneS H) : S1[A] } } ;
assume A3: a c= the topology of (HTopSpace H) ; ::_thesis: union a in the topology of (HTopSpace H)
A4: a = { (union A) where A is Subset of (StoneS H) : A in { A where A is Subset of (StoneS H) : S1[A] } }
proof
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { (union A) where A is Subset of (StoneS H) : A in { A where A is Subset of (StoneS H) : S1[A] } } c= a
let x be set ; ::_thesis: ( x in a implies x in { (union A) where A is Subset of (StoneS H) : A in { A where A is Subset of (StoneS H) : S1[A] } } )
assume A5: x in a ; ::_thesis: x in { (union A) where A is Subset of (StoneS H) : A in { A where A is Subset of (StoneS H) : S1[A] } }
then x in the topology of (HTopSpace H) by A3;
then consider A being Subset of (StoneS H) such that
A6: x = union A by A1;
A in { A where A is Subset of (StoneS H) : S1[A] } by A5, A6;
hence x in { (union A) where A is Subset of (StoneS H) : A in { A where A is Subset of (StoneS H) : S1[A] } } by A6; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (union A) where A is Subset of (StoneS H) : A in { A where A is Subset of (StoneS H) : S1[A] } } or x in a )
assume x in { (union A) where A is Subset of (StoneS H) : A in { A where A is Subset of (StoneS H) : S1[A] } } ; ::_thesis: x in a
then consider A being Subset of (StoneS H) such that
A7: x = union A and
A8: A in { A where A is Subset of (StoneS H) : S1[A] } ;
ex A9 being Subset of (StoneS H) st
( A = A9 & union A9 in a ) by A8;
hence x in a by A7; ::_thesis: verum
end;
reconsider B = { A where A is Subset of (StoneS H) : S1[A] } as Subset-Family of (StoneS H) from DOMAIN_1:sch_7();
union (union B) = union a by A4, EQREL_1:54;
hence union a in the topology of (HTopSpace H) by A1; ::_thesis: verum
end;
let a, b be Subset of (HTopSpace H); ::_thesis: ( not a in the topology of (HTopSpace H) or not b in the topology of (HTopSpace H) or a /\ b in the topology of (HTopSpace H) )
assume that
A9: a in the topology of (HTopSpace H) and
A10: b in the topology of (HTopSpace H) ; ::_thesis: a /\ b in the topology of (HTopSpace H)
consider A being Subset of (StoneS H) such that
A11: a = union A by A1, A9;
consider B being Subset of (StoneS H) such that
A12: b = union B by A1, A10;
INTERSECTION (A,B) c= StoneS H
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in INTERSECTION (A,B) or x in StoneS H )
assume x in INTERSECTION (A,B) ; ::_thesis: x in StoneS H
then consider X, Y being set such that
A13: X in A and
A14: Y in B and
A15: x = X /\ Y by SETFAM_1:def_5;
consider p9 being Element of H such that
A16: X = (StoneH H) . p9 by A13, Th13;
consider q9 being Element of H such that
A17: Y = (StoneH H) . q9 by A14, Th13;
x = (StoneH H) . (p9 "/\" q9) by A15, A16, A17, Th15;
hence x in StoneS H ; ::_thesis: verum
end;
then reconsider C = INTERSECTION (A,B) as Subset of (StoneS H) ;
(union A) /\ (union B) = union C by SETFAM_1:28;
hence a /\ b in the topology of (HTopSpace H) by A1, A11, A12; ::_thesis: verum
end;
end;
theorem :: OPENLATT:31
for H being non trivial H_Lattice holds the carrier of (Open_setLatt (HTopSpace H)) = { (union A) where A is Subset of (StoneS H) : verum } by Def12;
theorem Th32: :: OPENLATT:32
for H being non trivial H_Lattice holds StoneS H c= the carrier of (Open_setLatt (HTopSpace H))
proof
let H be non trivial H_Lattice; ::_thesis: StoneS H c= the carrier of (Open_setLatt (HTopSpace H))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in StoneS H or x in the carrier of (Open_setLatt (HTopSpace H)) )
set carrO = the carrier of (Open_setLatt (HTopSpace H));
assume x in StoneS H ; ::_thesis: x in the carrier of (Open_setLatt (HTopSpace H))
then reconsider z = {x} as Subset of (StoneS H) by ZFMISC_1:31;
A1: union z = x by ZFMISC_1:25;
the carrier of (Open_setLatt (HTopSpace H)) = { (union A) where A is Subset of (StoneS H) : verum } by Def12;
hence x in the carrier of (Open_setLatt (HTopSpace H)) by A1; ::_thesis: verum
end;
definition
let H be non trivial H_Lattice;
:: original: StoneH
redefine func StoneH H -> Homomorphism of H, Open_setLatt (HTopSpace H);
coherence
StoneH H is Homomorphism of H, Open_setLatt (HTopSpace H)
proof
set LH = Open_setLatt (HTopSpace H);
reconsider g = StoneH H as Function of the carrier of H, the carrier of (StoneLatt H) ;
StoneS H c= the carrier of (Open_setLatt (HTopSpace H)) by Th32;
then reconsider f = g as Function of the carrier of H, the carrier of (Open_setLatt (HTopSpace H)) by FUNCT_2:6;
now__::_thesis:_for_p9,_q9_being_Element_of_H_holds_
(_f_._(p9_"\/"_q9)_=_(f_._p9)_"\/"_(f_._q9)_&_f_._(p9_"/\"_q9)_=_(f_._p9)_"/\"_(f_._q9)_)
let p9, q9 be Element of H; ::_thesis: ( f . (p9 "\/" q9) = (f . p9) "\/" (f . q9) & f . (p9 "/\" q9) = (f . p9) "/\" (f . q9) )
thus f . (p9 "\/" q9) = ((StoneH H) . p9) \/ ((StoneH H) . q9) by Th14
.= (f . p9) "\/" (f . q9) by Def2 ; ::_thesis: f . (p9 "/\" q9) = (f . p9) "/\" (f . q9)
thus f . (p9 "/\" q9) = ((StoneH H) . p9) /\ ((StoneH H) . q9) by Th15
.= (f . p9) "/\" (f . q9) by Def3 ; ::_thesis: verum
end;
hence StoneH H is Homomorphism of H, Open_setLatt (HTopSpace H) by LATTICE4:def_1; ::_thesis: verum
end;
end;
theorem Th33: :: OPENLATT:33
for H being non trivial H_Lattice
for p9, q9 being Element of H holds (StoneH H) . (p9 => q9) = ((StoneH H) . p9) => ((StoneH H) . q9)
proof
let H be non trivial H_Lattice; ::_thesis: for p9, q9 being Element of H holds (StoneH H) . (p9 => q9) = ((StoneH H) . p9) => ((StoneH H) . q9)
let p9, q9 be Element of H; ::_thesis: (StoneH H) . (p9 => q9) = ((StoneH H) . p9) => ((StoneH H) . q9)
A1: the carrier of (Open_setLatt (HTopSpace H)) = { (union A) where A is Subset of (StoneS H) : verum } by Def12;
A2: now__::_thesis:_for_r_being_Element_of_(Open_setLatt_(HTopSpace_H))_st_((StoneH_H)_._p9)_"/\"_r_[=_(StoneH_H)_._q9_holds_
r_[=_(StoneH_H)_._(p9_=>_q9)
let r be Element of (Open_setLatt (HTopSpace H)); ::_thesis: ( ((StoneH H) . p9) "/\" r [= (StoneH H) . q9 implies r [= (StoneH H) . (p9 => q9) )
r in the carrier of (Open_setLatt (HTopSpace H)) ;
then consider A being Subset of (StoneS H) such that
A3: r = union A by A1;
assume ((StoneH H) . p9) "/\" r [= (StoneH H) . q9 ; ::_thesis: r [= (StoneH H) . (p9 => q9)
then ((StoneH H) . p9) "/\" r c= (StoneH H) . q9 by Th6;
then ((StoneH H) . p9) /\ (union A) c= (StoneH H) . q9 by A3, Def3;
then A4: union (INTERSECTION ({((StoneH H) . p9)},A)) c= (StoneH H) . q9 by SETFAM_1:25;
now__::_thesis:_for_x_being_set_st_x_in_A_holds_
x_c=_(StoneH_H)_._(p9_=>_q9)
let x be set ; ::_thesis: ( x in A implies x c= (StoneH H) . (p9 => q9) )
assume A5: x in A ; ::_thesis: x c= (StoneH H) . (p9 => q9)
then consider x9 being Element of H such that
A6: x = (StoneH H) . x9 by Th13;
(StoneH H) . p9 in {((StoneH H) . p9)} by TARSKI:def_1;
then ((StoneH H) . p9) /\ x in INTERSECTION ({((StoneH H) . p9)},A) by A5, SETFAM_1:def_5;
then ((StoneH H) . p9) /\ ((StoneH H) . x9) c= (StoneH H) . q9 by A4, A6, SETFAM_1:41;
then (StoneH H) . (p9 "/\" x9) c= (StoneH H) . q9 by Th15;
then (StoneH H) . (p9 "/\" x9) [= (StoneH H) . q9 by Th6;
then p9 "/\" x9 [= q9 by LATTICE4:5;
then x9 [= p9 => q9 by FILTER_0:def_7;
then (StoneH H) . x9 [= (StoneH H) . (p9 => q9) by LATTICE4:4;
hence x c= (StoneH H) . (p9 => q9) by A6, Th6; ::_thesis: verum
end;
then union A c= (StoneH H) . (p9 => q9) by ZFMISC_1:76;
hence r [= (StoneH H) . (p9 => q9) by A3, Th6; ::_thesis: verum
end;
p9 "/\" (p9 => q9) [= q9 by FILTER_0:def_7;
then (StoneH H) . (p9 "/\" (p9 => q9)) [= (StoneH H) . q9 by LATTICE4:4;
then ((StoneH H) . p9) "/\" ((StoneH H) . (p9 => q9)) [= (StoneH H) . q9 by LATTICE4:def_1;
hence (StoneH H) . (p9 => q9) = ((StoneH H) . p9) => ((StoneH H) . q9) by A2, FILTER_0:def_7; ::_thesis: verum
end;
theorem :: OPENLATT:34
for H being non trivial H_Lattice holds StoneH H preserves_implication
proof
let H be non trivial H_Lattice; ::_thesis: StoneH H preserves_implication
for p9, q9 being Element of H holds (StoneH H) . (p9 => q9) = ((StoneH H) . p9) => ((StoneH H) . q9) by Th33;
hence StoneH H preserves_implication by LATTICE4:def_3; ::_thesis: verum
end;
theorem :: OPENLATT:35
for H being non trivial H_Lattice holds StoneH H preserves_top
proof
let H be non trivial H_Lattice; ::_thesis: StoneH H preserves_top
(StoneH H) . (Top H) = F_primeSet H by Th28
.= the carrier of (HTopSpace H) by Def12
.= Top (Open_setLatt (HTopSpace H)) by Th9 ;
hence StoneH H preserves_top by LATTICE4:def_4; ::_thesis: verum
end;
theorem :: OPENLATT:36
for H being non trivial H_Lattice holds StoneH H preserves_bottom
proof
let H be non trivial H_Lattice; ::_thesis: StoneH H preserves_bottom
(StoneH H) . (Bottom H) = {} by Th29
.= Bottom (Open_setLatt (HTopSpace H)) by Th8 ;
hence StoneH H preserves_bottom by LATTICE4:def_5; ::_thesis: verum
end;