:: 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;