:: TEX_2 semantic presentation begin theorem Th1: :: TEX_2:1 for A being non empty set for B being 1 -element set st A c= B holds A = B proof let A be non empty set ; ::_thesis: for B being 1 -element set st A c= B holds A = B let B be 1 -element set ; ::_thesis: ( A c= B implies A = B ) assume A1: A c= B ; ::_thesis: A = B ex s being Element of B st B = {s} by SUBSET_1:46; hence A = B by A1, ZFMISC_1:33; ::_thesis: verum end; theorem :: TEX_2:2 for A being 1 -element set for B being set st not A /\ B is empty holds A c= B proof let A be 1 -element set ; ::_thesis: for B being set st not A /\ B is empty holds A c= B let B be set ; ::_thesis: ( not A /\ B is empty implies A c= B ) A1: A /\ B c= B by XBOOLE_1:17; assume not A /\ B is empty ; ::_thesis: A c= B then consider a being set such that A2: a in A /\ B by XBOOLE_0:def_1; A3: ex s being Element of A st A = {s} by SUBSET_1:46; A /\ B c= A by XBOOLE_1:17; then {a} c= A by A2, ZFMISC_1:31; then {a} = A by A3, ZFMISC_1:18; hence A c= B by A2, A1, ZFMISC_1:31; ::_thesis: verum end; registration let S be 1 -element set ; cluster proper -> empty for Element of bool S; coherence for b1 being Subset of S st b1 is proper holds b1 is empty proof let A be Subset of S; ::_thesis: ( A is proper implies A is empty ) assume A is proper ; ::_thesis: A is empty then A1: A <> S by SUBSET_1:def_6; ex s being Element of S st S = {s} by SUBSET_1:46; hence A is empty by A1, ZFMISC_1:33; ::_thesis: verum end; cluster non empty -> non proper for Element of bool S; coherence for b1 being Subset of S st not b1 is empty holds not b1 is proper ; end; theorem :: TEX_2:3 for S being non empty set for y being Element of S st {y} is proper holds not S is trivial ; theorem :: TEX_2:4 for S being non trivial set for y being Element of S holds {y} is proper by SUBSET_1:def_6; registration let S be 1 -element set ; cluster non empty non proper -> non empty trivial for Element of bool S; coherence for b1 being non empty Subset of S st not b1 is proper holds b1 is trivial ; end; registration let S be non trivial set ; cluster non empty trivial -> non empty proper for Element of bool S; coherence for b1 being non empty Subset of S st b1 is trivial holds b1 is proper by SUBSET_1:def_6; cluster non empty non proper -> non empty non trivial for Element of bool S; coherence for b1 being non empty Subset of S st not b1 is proper holds not b1 is trivial ; end; registration let S be non trivial set ; cluster non empty trivial proper for Element of bool S; existence ex b1 being non empty Subset of S st ( b1 is trivial & b1 is proper ) proof set A = the non empty trivial Subset of S; take the non empty trivial Subset of S ; ::_thesis: ( the non empty trivial Subset of S is trivial & the non empty trivial Subset of S is proper ) thus ( the non empty trivial Subset of S is trivial & the non empty trivial Subset of S is proper ) ; ::_thesis: verum end; cluster non empty non trivial non proper for Element of bool S; existence ex b1 being non empty Subset of S st ( not b1 is trivial & not b1 is proper ) proof take [#] S ; ::_thesis: ( not [#] S is trivial & not [#] S is proper ) thus ( not [#] S is trivial & not [#] S is proper ) ; ::_thesis: verum end; end; theorem :: TEX_2:5 for Y being non empty 1-sorted for y being Element of Y st {y} is proper holds not Y is trivial ; theorem :: TEX_2:6 for Y being non trivial 1-sorted for y being Element of Y holds {y} is proper ; registration let Y be 1 -element 1-sorted ; cluster non empty -> non empty non proper for Element of bool the carrier of Y; coherence for b1 being non empty Subset of Y holds not b1 is proper ; cluster non empty non proper -> non empty trivial for Element of bool the carrier of Y; coherence for b1 being non empty Subset of Y st not b1 is proper holds b1 is trivial ; end; registration let Y be non trivial 1-sorted ; cluster non empty trivial -> non empty proper for Element of bool the carrier of Y; coherence for b1 being non empty Subset of Y st b1 is trivial holds b1 is proper ; cluster non empty non proper -> non empty non trivial for Element of bool the carrier of Y; coherence for b1 being non empty Subset of Y st not b1 is proper holds not b1 is trivial ; end; registration let Y be non trivial 1-sorted ; cluster non empty trivial proper for Element of bool the carrier of Y; existence ex b1 being non empty Subset of Y st ( b1 is trivial & b1 is proper ) proof set A = the non empty trivial Subset of Y; take the non empty trivial Subset of Y ; ::_thesis: ( the non empty trivial Subset of Y is trivial & the non empty trivial Subset of Y is proper ) thus ( the non empty trivial Subset of Y is trivial & the non empty trivial Subset of Y is proper ) ; ::_thesis: verum end; cluster non empty non trivial non proper for Element of bool the carrier of Y; existence ex b1 being non empty Subset of Y st ( not b1 is trivial & not b1 is proper ) proof take [#] Y ; ::_thesis: ( not [#] Y is trivial & not [#] Y is proper ) thus ( not [#] Y is trivial & not [#] Y is proper ) ; ::_thesis: verum end; end; registration let Y be non trivial 1-sorted ; cluster non empty trivial proper for Element of bool the carrier of Y; existence ex b1 being Subset of Y st ( not b1 is empty & b1 is trivial & b1 is proper ) proof set X = the non empty trivial proper Subset of Y; reconsider X = the non empty trivial proper Subset of Y as Subset of Y ; take X ; ::_thesis: ( not X is empty & X is trivial & X is proper ) thus ( not X is empty & X is trivial & X is proper ) ; ::_thesis: verum end; end; registration let X be non empty set ; let A be proper Subset of X; clusterA ` -> non empty ; coherence not A ` is empty proof assume A ` is empty ; ::_thesis: contradiction then (A `) ` = X ; hence contradiction by SUBSET_1:def_6; ::_thesis: verum end; end; begin theorem :: TEX_2:7 for Y0, Y1 being TopStruct st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & Y0 is TopSpace-like holds Y1 is TopSpace-like proof let Y0, Y1 be TopStruct ; ::_thesis: ( TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & Y0 is TopSpace-like implies Y1 is TopSpace-like ) assume A1: TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) ; ::_thesis: ( not Y0 is TopSpace-like or Y1 is TopSpace-like ) assume A2: Y0 is TopSpace-like ; ::_thesis: Y1 is TopSpace-like hence the carrier of Y1 in the topology of Y1 by A1, PRE_TOPC:def_1; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of bool (bool the carrier of Y1) holds ( not b1 c= the topology of Y1 or union b1 in the topology of Y1 ) ) & ( for b1, b2 being Element of bool the carrier of Y1 holds ( not b1 in the topology of Y1 or not b2 in the topology of Y1 or b1 /\ b2 in the topology of Y1 ) ) ) thus ( ( for b1 being Element of bool (bool the carrier of Y1) holds ( not b1 c= the topology of Y1 or union b1 in the topology of Y1 ) ) & ( for b1, b2 being Element of bool the carrier of Y1 holds ( not b1 in the topology of Y1 or not b2 in the topology of Y1 or b1 /\ b2 in the topology of Y1 ) ) ) by A1, A2, PRE_TOPC:def_1; ::_thesis: verum end; definition let Y be TopStruct ; let IT be SubSpace of Y; attrIT is proper means :Def1: :: TEX_2:def 1 for A being Subset of Y st A = the carrier of IT holds A is proper ; end; :: deftheorem Def1 defines proper TEX_2:def_1_:_ for Y being TopStruct for IT being SubSpace of Y holds ( IT is proper iff for A being Subset of Y st A = the carrier of IT holds A is proper ); theorem Th8: :: TEX_2:8 for Y being TopStruct for Y0 being SubSpace of Y for A being Subset of Y st A = the carrier of Y0 holds ( A is proper iff Y0 is proper ) proof let Y be TopStruct ; ::_thesis: for Y0 being SubSpace of Y for A being Subset of Y st A = the carrier of Y0 holds ( A is proper iff Y0 is proper ) let Y0 be SubSpace of Y; ::_thesis: for A being Subset of Y st A = the carrier of Y0 holds ( A is proper iff Y0 is proper ) let A be Subset of Y; ::_thesis: ( A = the carrier of Y0 implies ( A is proper iff Y0 is proper ) ) assume A1: A = the carrier of Y0 ; ::_thesis: ( A is proper iff Y0 is proper ) hereby ::_thesis: ( Y0 is proper implies A is proper ) assume A is proper ; ::_thesis: Y0 is proper then for A being Subset of Y st A = the carrier of Y0 holds A is proper by A1; hence Y0 is proper by Def1; ::_thesis: verum end; thus ( Y0 is proper implies A is proper ) by A1, Def1; ::_thesis: verum end; Lm1: now__::_thesis:_for_Z_being_TopStruct_ for_Z0_being_SubSpace_of_Z_holds_the_carrier_of_Z0_is_Subset_of_Z let Z be TopStruct ; ::_thesis: for Z0 being SubSpace of Z holds the carrier of Z0 is Subset of Z let Z0 be SubSpace of Z; ::_thesis: the carrier of Z0 is Subset of Z [#] Z0 c= [#] Z by PRE_TOPC:def_4; hence the carrier of Z0 is Subset of Z ; ::_thesis: verum end; theorem :: TEX_2:9 for Y being TopStruct for Y0, Y1 being SubSpace of Y st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & Y0 is proper holds Y1 is proper proof let Y be TopStruct ; ::_thesis: for Y0, Y1 being SubSpace of Y st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & Y0 is proper holds Y1 is proper let Y0, Y1 be SubSpace of Y; ::_thesis: ( TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & Y0 is proper implies Y1 is proper ) assume A1: TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) ; ::_thesis: ( not Y0 is proper or Y1 is proper ) assume Y0 is proper ; ::_thesis: Y1 is proper then for A being Subset of Y st A = the carrier of Y1 holds A is proper by A1, Def1; hence Y1 is proper by Def1; ::_thesis: verum end; theorem Th10: :: TEX_2:10 for Y being TopStruct for Y0 being SubSpace of Y st the carrier of Y0 = the carrier of Y holds not Y0 is proper proof let Y be TopStruct ; ::_thesis: for Y0 being SubSpace of Y st the carrier of Y0 = the carrier of Y holds not Y0 is proper let Y0 be SubSpace of Y; ::_thesis: ( the carrier of Y0 = the carrier of Y implies not Y0 is proper ) reconsider A = the carrier of Y0 as Subset of Y by Lm1; assume A1: the carrier of Y0 = the carrier of Y ; ::_thesis: not Y0 is proper now__::_thesis:_ex_A_being_Subset_of_Y_st_ (_A_=_the_carrier_of_Y0_&_not_A_is_proper_) take A = A; ::_thesis: ( A = the carrier of Y0 & not A is proper ) thus ( A = the carrier of Y0 & not A is proper ) by A1, SUBSET_1:def_6; ::_thesis: verum end; hence not Y0 is proper by Def1; ::_thesis: verum end; registration let Y be 1 -element TopStruct ; cluster non empty -> non empty non proper for SubSpace of Y; coherence for b1 being non empty SubSpace of Y holds not b1 is proper proof let Y0 be non empty SubSpace of Y; ::_thesis: not Y0 is proper reconsider A = the carrier of Y0 as non empty Subset of Y by Lm1; now__::_thesis:_ex_A_being_non_empty_Subset_of_Y_st_ (_A_=_the_carrier_of_Y0_&_not_A_is_proper_) take A = A; ::_thesis: ( A = the carrier of Y0 & not A is proper ) thus ( A = the carrier of Y0 & not A is proper ) ; ::_thesis: verum end; hence not Y0 is proper by Def1; ::_thesis: verum end; cluster non empty non proper -> non empty trivial for SubSpace of Y; coherence for b1 being non empty SubSpace of Y st not b1 is proper holds b1 is trivial proof let Y0 be non empty SubSpace of Y; ::_thesis: ( not Y0 is proper implies Y0 is trivial ) assume not Y0 is proper ; ::_thesis: Y0 is trivial ex A being Subset of Y st ( A = the carrier of Y0 & not A is proper ) by Def1; then reconsider A = the carrier of Y0 as non empty Subset of Y ; A is trivial ; hence Y0 is trivial ; ::_thesis: verum end; end; registration let Y be non trivial TopStruct ; cluster non empty trivial -> non empty proper for SubSpace of Y; coherence for b1 being non empty SubSpace of Y st b1 is trivial holds b1 is proper proof let Y0 be non empty SubSpace of Y; ::_thesis: ( Y0 is trivial implies Y0 is proper ) assume Y0 is trivial ; ::_thesis: Y0 is proper then for A being Subset of Y st A = the carrier of Y0 holds A is proper ; hence Y0 is proper by Def1; ::_thesis: verum end; cluster non empty non proper -> non empty non trivial for SubSpace of Y; coherence for b1 being non empty SubSpace of Y st not b1 is proper holds not b1 is trivial ; end; registration let Y be non empty TopStruct ; cluster non empty strict non proper for SubSpace of Y; existence ex b1 being SubSpace of Y st ( not b1 is proper & b1 is strict & not b1 is empty ) proof [#] Y = the carrier of Y ; then reconsider A0 = the carrier of Y as non empty Subset of Y ; set Y0 = Y | A0; take Y | A0 ; ::_thesis: ( not Y | A0 is proper & Y | A0 is strict & not Y | A0 is empty ) A0 = [#] (Y | A0) by PRE_TOPC:def_5; hence ( not Y | A0 is proper & Y | A0 is strict & not Y | A0 is empty ) by Th10; ::_thesis: verum end; end; theorem :: TEX_2:11 for Y being non empty TopStruct for Y0 being non proper SubSpace of Y holds TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y, the topology of Y #) proof let Y be non empty TopStruct ; ::_thesis: for Y0 being non proper SubSpace of Y holds TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y, the topology of Y #) let Y0 be non proper SubSpace of Y; ::_thesis: TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y, the topology of Y #) A1: ex A being Subset of Y st ( A = the carrier of Y0 & not A is proper ) by Def1; now__::_thesis:_for_D_being_set_st_D_in_the_topology_of_Y_holds_ D_in_the_topology_of_Y0 let D be set ; ::_thesis: ( D in the topology of Y implies D in the topology of Y0 ) assume A2: D in the topology of Y ; ::_thesis: D in the topology of Y0 then reconsider E = D as Subset of Y ; reconsider C = E as Subset of Y0 by A1, SUBSET_1:def_6; now__::_thesis:_ex_E_being_Subset_of_Y_st_ (_E_in_the_topology_of_Y_&_C_=_E_/\_([#]_Y0)_) take E = E; ::_thesis: ( E in the topology of Y & C = E /\ ([#] Y0) ) thus ( E in the topology of Y & C = E /\ ([#] Y0) ) by A2, XBOOLE_1:28; ::_thesis: verum end; hence D in the topology of Y0 by PRE_TOPC:def_4; ::_thesis: verum end; then A3: the topology of Y c= the topology of Y0 by TARSKI:def_3; A4: the carrier of Y0 = the carrier of Y by A1, SUBSET_1:def_6; now__::_thesis:_for_D_being_set_st_D_in_the_topology_of_Y0_holds_ D_in_the_topology_of_Y let D be set ; ::_thesis: ( D in the topology of Y0 implies D in the topology of Y ) assume A5: D in the topology of Y0 ; ::_thesis: D in the topology of Y then reconsider C = D as Subset of Y0 ; ex E being Subset of Y st ( E in the topology of Y & C = E /\ ([#] Y0) ) by A5, PRE_TOPC:def_4; hence D in the topology of Y by A4, XBOOLE_1:28; ::_thesis: verum end; then the topology of Y0 c= the topology of Y by TARSKI:def_3; then the topology of Y0 = the topology of Y by A3, XBOOLE_0:def_10; hence TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y, the topology of Y #) by A1, SUBSET_1:def_6; ::_thesis: verum end; registration let Y be non empty TopStruct ; cluster discrete -> TopSpace-like for SubSpace of Y; coherence for b1 being SubSpace of Y st b1 is discrete holds b1 is TopSpace-like ; cluster anti-discrete -> TopSpace-like for SubSpace of Y; coherence for b1 being SubSpace of Y st b1 is anti-discrete holds b1 is TopSpace-like ; cluster non TopSpace-like -> non discrete for SubSpace of Y; coherence for b1 being SubSpace of Y st not b1 is TopSpace-like holds not b1 is discrete ; cluster non TopSpace-like -> non anti-discrete for SubSpace of Y; coherence for b1 being SubSpace of Y st not b1 is TopSpace-like holds not b1 is anti-discrete ; end; theorem Th12: :: TEX_2:12 for Y0, Y1 being TopStruct st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & Y0 is discrete holds Y1 is discrete proof let Y0, Y1 be TopStruct ; ::_thesis: ( TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & Y0 is discrete implies Y1 is discrete ) assume A1: TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) ; ::_thesis: ( not Y0 is discrete or Y1 is discrete ) assume Y0 is discrete ; ::_thesis: Y1 is discrete then the topology of Y0 = bool the carrier of Y0 by TDLAT_3:def_1; hence Y1 is discrete by A1, TDLAT_3:def_1; ::_thesis: verum end; theorem :: TEX_2:13 for Y0, Y1 being TopStruct st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & Y0 is anti-discrete holds Y1 is anti-discrete proof let Y0, Y1 be TopStruct ; ::_thesis: ( TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & Y0 is anti-discrete implies Y1 is anti-discrete ) assume A1: TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) ; ::_thesis: ( not Y0 is anti-discrete or Y1 is anti-discrete ) assume Y0 is anti-discrete ; ::_thesis: Y1 is anti-discrete then the topology of Y0 = {{}, the carrier of Y0} by TDLAT_3:def_2; hence Y1 is anti-discrete by A1, TDLAT_3:def_2; ::_thesis: verum end; registration let Y be non empty TopStruct ; cluster discrete -> almost_discrete for SubSpace of Y; coherence for b1 being SubSpace of Y st b1 is discrete holds b1 is almost_discrete ; cluster non almost_discrete -> non discrete for SubSpace of Y; coherence for b1 being SubSpace of Y st not b1 is almost_discrete holds not b1 is discrete ; cluster anti-discrete -> almost_discrete for SubSpace of Y; coherence for b1 being SubSpace of Y st b1 is anti-discrete holds b1 is almost_discrete ; cluster non almost_discrete -> non anti-discrete for SubSpace of Y; coherence for b1 being SubSpace of Y st not b1 is almost_discrete holds not b1 is anti-discrete ; end; theorem :: TEX_2:14 for Y0, Y1 being TopStruct st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & Y0 is almost_discrete holds Y1 is almost_discrete proof let Y0, Y1 be TopStruct ; ::_thesis: ( TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & Y0 is almost_discrete implies Y1 is almost_discrete ) assume A1: TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) ; ::_thesis: ( not Y0 is almost_discrete or Y1 is almost_discrete ) assume Y0 is almost_discrete ; ::_thesis: Y1 is almost_discrete then for A being Subset of Y0 st A in the topology of Y0 holds the carrier of Y0 \ A in the topology of Y0 by TDLAT_3:def_3; hence Y1 is almost_discrete by A1, TDLAT_3:def_3; ::_thesis: verum end; registration let Y be non empty TopStruct ; cluster non empty discrete anti-discrete -> non empty trivial for SubSpace of Y; coherence for b1 being non empty SubSpace of Y st b1 is discrete & b1 is anti-discrete holds b1 is trivial ; cluster non empty non trivial anti-discrete -> non empty non discrete for SubSpace of Y; coherence for b1 being non empty SubSpace of Y st b1 is anti-discrete & not b1 is trivial holds not b1 is discrete ; cluster non empty non trivial discrete -> non empty non anti-discrete for SubSpace of Y; coherence for b1 being non empty SubSpace of Y st b1 is discrete & not b1 is trivial holds not b1 is anti-discrete ; end; definition let Y be non empty TopStruct ; let y be Point of Y; func Sspace y -> non empty strict SubSpace of Y means :Def2: :: TEX_2:def 2 the carrier of it = {y}; existence ex b1 being non empty strict SubSpace of Y st the carrier of b1 = {y} proof reconsider D = {y} as non empty Subset of Y ; set Y0 = Y | D; take Y | D ; ::_thesis: the carrier of (Y | D) = {y} D = [#] (Y | D) by PRE_TOPC:def_5; hence the carrier of (Y | D) = {y} ; ::_thesis: verum end; uniqueness for b1, b2 being non empty strict SubSpace of Y st the carrier of b1 = {y} & the carrier of b2 = {y} holds b1 = b2 proof let Y1, Y2 be non empty strict SubSpace of Y; ::_thesis: ( the carrier of Y1 = {y} & the carrier of Y2 = {y} implies Y1 = Y2 ) assume that A1: the carrier of Y1 = {y} and A2: the carrier of Y2 = {y} ; ::_thesis: Y1 = Y2 set A1 = the carrier of Y1; set A2 = the carrier of Y2; A3: the carrier of Y2 = [#] Y2 ; A4: the carrier of Y1 = [#] Y1 ; then the carrier of Y1 c= [#] Y by PRE_TOPC:def_4; then reconsider A1 = the carrier of Y1 as Subset of Y ; Y1 = Y | A1 by A4, PRE_TOPC:def_5; hence Y1 = Y2 by A1, A2, A3, PRE_TOPC:def_5; ::_thesis: verum end; end; :: deftheorem Def2 defines Sspace TEX_2:def_2_:_ for Y being non empty TopStruct for y being Point of Y for b3 being non empty strict SubSpace of Y holds ( b3 = Sspace y iff the carrier of b3 = {y} ); Lm2: now__::_thesis:_for_Y_being_non_empty_TopStruct_ for_y_being_Point_of_Y_holds_Sspace_y_is_1_-element let Y be non empty TopStruct ; ::_thesis: for y being Point of Y holds Sspace y is 1 -element let y be Point of Y; ::_thesis: Sspace y is 1 -element set Y0 = Sspace y; the carrier of (Sspace y) = {y} by Def2; then reconsider y0 = y as Point of (Sspace y) by TARSKI:def_1; the carrier of (Sspace y) = {y0} by Def2; hence Sspace y is 1 -element by STRUCT_0:def_19; ::_thesis: verum end; registration let Y be non empty TopStruct ; cluster1 -element strict for SubSpace of Y; existence ex b1 being SubSpace of Y st ( b1 is strict & b1 is 1 -element ) proof set y = the Point of Y; take Sspace the Point of Y ; ::_thesis: ( Sspace the Point of Y is strict & Sspace the Point of Y is 1 -element ) thus ( Sspace the Point of Y is strict & Sspace the Point of Y is 1 -element ) by Lm2; ::_thesis: verum end; end; registration let Y be non empty TopStruct ; let y be Point of Y; cluster Sspace y -> non empty 1 -element strict ; coherence Sspace y is 1 -element by Lm2; end; theorem :: TEX_2:15 for Y being non empty TopStruct for y being Point of Y holds ( Sspace y is proper iff {y} is proper ) proof let Y be non empty TopStruct ; ::_thesis: for y being Point of Y holds ( Sspace y is proper iff {y} is proper ) let y be Point of Y; ::_thesis: ( Sspace y is proper iff {y} is proper ) hereby ::_thesis: ( {y} is proper implies Sspace y is proper ) reconsider A = the carrier of (Sspace y) as Subset of Y by Lm1; assume A1: Sspace y is proper ; ::_thesis: {y} is proper A = {y} by Def2; hence {y} is proper by A1, Def1; ::_thesis: verum end; hereby ::_thesis: verum assume {y} is proper ; ::_thesis: Sspace y is proper then for A being Subset of Y st A = the carrier of (Sspace y) holds A is proper by Def2; hence Sspace y is proper by Def1; ::_thesis: verum end; end; theorem :: TEX_2:16 for Y being non empty TopStruct for y being Point of Y st Sspace y is proper holds not Y is trivial ; registration let Y be non trivial TopStruct ; cluster non empty trivial strict proper for SubSpace of Y; existence ex b1 being non empty SubSpace of Y st ( b1 is proper & b1 is trivial & b1 is strict ) proof set Y0 = the non empty trivial strict SubSpace of Y; take the non empty trivial strict SubSpace of Y ; ::_thesis: ( the non empty trivial strict SubSpace of Y is proper & the non empty trivial strict SubSpace of Y is trivial & the non empty trivial strict SubSpace of Y is strict ) thus ( the non empty trivial strict SubSpace of Y is proper & the non empty trivial strict SubSpace of Y is trivial & the non empty trivial strict SubSpace of Y is strict ) ; ::_thesis: verum end; end; registration let Y be non empty TopStruct ; cluster1 -element for SubSpace of Y; existence ex b1 being SubSpace of Y st b1 is 1 -element proof take Y0 = the non empty trivial SubSpace of Y; ::_thesis: Y0 is 1 -element thus Y0 is 1 -element ; ::_thesis: verum end; end; theorem :: TEX_2:17 for Y being non empty TopStruct for Y0 being 1 -element SubSpace of Y ex y being Point of Y st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of (Sspace y), the topology of (Sspace y) #) proof let Y be non empty TopStruct ; ::_thesis: for Y0 being 1 -element SubSpace of Y ex y being Point of Y st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of (Sspace y), the topology of (Sspace y) #) let Y0 be 1 -element SubSpace of Y; ::_thesis: ex y being Point of Y st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of (Sspace y), the topology of (Sspace y) #) consider y0 being Element of Y0 such that A1: the carrier of Y0 = {y0} by TEX_1:def_1; the carrier of Y0 is Subset of Y by Lm1; then reconsider y = y0 as Point of Y by A1, ZFMISC_1:31; take y ; ::_thesis: TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of (Sspace y), the topology of (Sspace y) #) the carrier of Y0 = the carrier of (Sspace y) by A1, Def2; hence TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of (Sspace y), the topology of (Sspace y) #) by TSEP_1:5; ::_thesis: verum end; theorem :: TEX_2:18 for Y being non empty TopStruct for y being Point of Y st Sspace y is TopSpace-like holds ( Sspace y is discrete & Sspace y is anti-discrete ) ; registration let Y be non empty TopStruct ; cluster non empty trivial TopSpace-like -> non empty discrete anti-discrete for SubSpace of Y; coherence for b1 being non empty SubSpace of Y st b1 is trivial & b1 is TopSpace-like holds ( b1 is discrete & b1 is anti-discrete ) ; end; registration let X be non empty TopSpace; cluster non empty trivial strict TopSpace-like for SubSpace of X; existence ex b1 being SubSpace of X st ( b1 is trivial & b1 is strict & b1 is TopSpace-like & not b1 is empty ) proof set x = the Point of X; take Sspace the Point of X ; ::_thesis: ( Sspace the Point of X is trivial & Sspace the Point of X is strict & Sspace the Point of X is TopSpace-like & not Sspace the Point of X is empty ) thus ( Sspace the Point of X is trivial & Sspace the Point of X is strict & Sspace the Point of X is TopSpace-like & not Sspace the Point of X is empty ) ; ::_thesis: verum end; end; registration let X be non empty TopSpace; let x be Point of X; cluster Sspace x -> non empty strict TopSpace-like ; coherence Sspace x is TopSpace-like ; end; registration let X be non empty TopSpace; cluster non empty strict TopSpace-like discrete anti-discrete for SubSpace of X; existence ex b1 being SubSpace of X st ( b1 is discrete & b1 is anti-discrete & b1 is strict & not b1 is empty ) proof set x = the Point of X; take Sspace the Point of X ; ::_thesis: ( Sspace the Point of X is discrete & Sspace the Point of X is anti-discrete & Sspace the Point of X is strict & not Sspace the Point of X is empty ) thus ( Sspace the Point of X is discrete & Sspace the Point of X is anti-discrete & Sspace the Point of X is strict & not Sspace the Point of X is empty ) ; ::_thesis: verum end; end; registration let X be non empty TopSpace; let x be Point of X; cluster Sspace x -> non empty strict discrete anti-discrete ; coherence ( Sspace x is discrete & Sspace x is anti-discrete ) ; end; registration let X be non empty TopSpace; cluster non proper -> closed open for SubSpace of X; coherence for b1 being SubSpace of X st not b1 is proper holds ( b1 is open & b1 is closed ) proof let X0 be SubSpace of X; ::_thesis: ( not X0 is proper implies ( X0 is open & X0 is closed ) ) assume not X0 is proper ; ::_thesis: ( X0 is open & X0 is closed ) then A1: ex A being Subset of X st ( A = the carrier of X0 & not A is proper ) by Def1; A2: now__::_thesis:_for_A_being_Subset_of_X_st_A_=_the_carrier_of_X0_holds_ A_is_closed let A be Subset of X; ::_thesis: ( A = the carrier of X0 implies A is closed ) assume A = the carrier of X0 ; ::_thesis: A is closed then A = [#] X by A1, SUBSET_1:def_6; hence A is closed ; ::_thesis: verum end; now__::_thesis:_for_A_being_Subset_of_X_st_A_=_the_carrier_of_X0_holds_ A_is_open let A be Subset of X; ::_thesis: ( A = the carrier of X0 implies A is open ) assume A = the carrier of X0 ; ::_thesis: A is open then A = [#] X by A1, SUBSET_1:def_6; hence A is open ; ::_thesis: verum end; hence ( X0 is open & X0 is closed ) by A2, BORSUK_1:def_11, TSEP_1:def_1; ::_thesis: verum end; cluster non open -> proper for SubSpace of X; coherence for b1 being SubSpace of X st not b1 is open holds b1 is proper ; cluster non closed -> proper for SubSpace of X; coherence for b1 being SubSpace of X st not b1 is closed holds b1 is proper ; end; registration let X be non empty TopSpace; cluster strict TopSpace-like closed open for SubSpace of X; existence ex b1 being SubSpace of X st ( b1 is open & b1 is closed & b1 is strict ) proof set X0 = the strict non proper SubSpace of X; take the strict non proper SubSpace of X ; ::_thesis: ( the strict non proper SubSpace of X is open & the strict non proper SubSpace of X is closed & the strict non proper SubSpace of X is strict ) thus ( the strict non proper SubSpace of X is open & the strict non proper SubSpace of X is closed & the strict non proper SubSpace of X is strict ) ; ::_thesis: verum end; end; registration let X be non empty discrete TopSpace; cluster non empty anti-discrete -> non empty trivial for SubSpace of X; coherence for b1 being non empty SubSpace of X st b1 is anti-discrete holds b1 is trivial ; cluster non empty non trivial -> non empty non anti-discrete for SubSpace of X; coherence for b1 being non empty SubSpace of X st not b1 is trivial holds not b1 is anti-discrete ; end; registration let X be non trivial discrete TopSpace; cluster strict TopSpace-like closed open discrete almost_discrete proper for SubSpace of X; existence ex b1 being SubSpace of X st ( b1 is discrete & b1 is open & b1 is closed & b1 is proper & b1 is strict ) proof set X0 = the strict proper SubSpace of X; take the strict proper SubSpace of X ; ::_thesis: ( the strict proper SubSpace of X is discrete & the strict proper SubSpace of X is open & the strict proper SubSpace of X is closed & the strict proper SubSpace of X is proper & the strict proper SubSpace of X is strict ) thus ( the strict proper SubSpace of X is discrete & the strict proper SubSpace of X is open & the strict proper SubSpace of X is closed & the strict proper SubSpace of X is proper & the strict proper SubSpace of X is strict ) ; ::_thesis: verum end; end; registration let X be non empty anti-discrete TopSpace; cluster non empty discrete -> non empty trivial for SubSpace of X; coherence for b1 being non empty SubSpace of X st b1 is discrete holds b1 is trivial ; cluster non empty non trivial -> non empty non discrete for SubSpace of X; coherence for b1 being non empty SubSpace of X st not b1 is trivial holds not b1 is discrete ; end; registration let X be non trivial anti-discrete TopSpace; cluster non empty proper -> non empty non closed non open proper for SubSpace of X; coherence for b1 being non empty proper SubSpace of X holds ( not b1 is open & not b1 is closed ) proof let X0 be non empty proper SubSpace of X; ::_thesis: ( not X0 is open & not X0 is closed ) assume A1: ( X0 is open or X0 is closed ) ; ::_thesis: contradiction reconsider A = the carrier of X0 as non empty Subset of X by Lm1; set B = A ` ; A2: A ` <> the carrier of X by TOPS_3:1; A3: A is proper by Def1; then A4: A <> the carrier of X by SUBSET_1:def_6; now__::_thesis:_contradiction percases ( X0 is open or X0 is closed ) by A1; suppose X0 is open ; ::_thesis: contradiction then A is open by TSEP_1:def_1; then A in the topology of X by PRE_TOPC:def_2; then A in {{}, the carrier of X} by TDLAT_3:def_2; hence contradiction by A4, TARSKI:def_2; ::_thesis: verum end; suppose X0 is closed ; ::_thesis: contradiction then A is closed by BORSUK_1:def_11; then A ` in the topology of X by PRE_TOPC:def_2; then A ` in {{}, the carrier of X} by TDLAT_3:def_2; hence contradiction by A3, A2, TARSKI:def_2; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; cluster non empty discrete -> non empty trivial discrete proper for SubSpace of X; coherence for b1 being non empty discrete SubSpace of X holds ( b1 is trivial & b1 is proper ) ; end; registration let X be non trivial anti-discrete TopSpace; cluster strict TopSpace-like non closed non open anti-discrete almost_discrete proper for SubSpace of X; existence ex b1 being SubSpace of X st ( b1 is anti-discrete & not b1 is open & not b1 is closed & b1 is proper & b1 is strict ) proof set X0 = the non empty strict proper SubSpace of X; take the non empty strict proper SubSpace of X ; ::_thesis: ( the non empty strict proper SubSpace of X is anti-discrete & not the non empty strict proper SubSpace of X is open & not the non empty strict proper SubSpace of X is closed & the non empty strict proper SubSpace of X is proper & the non empty strict proper SubSpace of X is strict ) thus ( the non empty strict proper SubSpace of X is anti-discrete & not the non empty strict proper SubSpace of X is open & not the non empty strict proper SubSpace of X is closed & the non empty strict proper SubSpace of X is proper & the non empty strict proper SubSpace of X is strict ) ; ::_thesis: verum end; end; registration let X be non trivial almost_discrete TopSpace; cluster non empty strict TopSpace-like almost_discrete proper for SubSpace of X; existence ex b1 being SubSpace of X st ( b1 is almost_discrete & b1 is proper & b1 is strict & not b1 is empty ) proof set X0 = the non empty strict proper SubSpace of X; take the non empty strict proper SubSpace of X ; ::_thesis: ( the non empty strict proper SubSpace of X is almost_discrete & the non empty strict proper SubSpace of X is proper & the non empty strict proper SubSpace of X is strict & not the non empty strict proper SubSpace of X is empty ) thus ( the non empty strict proper SubSpace of X is almost_discrete & the non empty strict proper SubSpace of X is proper & the non empty strict proper SubSpace of X is strict & not the non empty strict proper SubSpace of X is empty ) ; ::_thesis: verum end; end; begin definition let Y be TopStruct ; let IT be Subset of Y; attrIT is discrete means :Def3: :: TEX_2:def 3 for D being Subset of Y st D c= IT holds ex G being Subset of Y st ( G is open & IT /\ G = D ); end; :: deftheorem Def3 defines discrete TEX_2:def_3_:_ for Y being TopStruct for IT being Subset of Y holds ( IT is discrete iff for D being Subset of Y st D c= IT holds ex G being Subset of Y st ( G is open & IT /\ G = D ) ); definition let Y be TopStruct ; let A be Subset of Y; redefine attr A is discrete means :Def4: :: TEX_2:def 4 for D being Subset of Y st D c= A holds ex F being Subset of Y st ( F is closed & A /\ F = D ); compatibility ( A is discrete iff for D being Subset of Y st D c= A holds ex F being Subset of Y st ( F is closed & A /\ F = D ) ) proof hereby ::_thesis: ( ( for D being Subset of Y st D c= A holds ex F being Subset of Y st ( F is closed & A /\ F = D ) ) implies A is discrete ) assume A1: A is discrete ; ::_thesis: for D being Subset of Y st D c= A holds ex F being Subset of Y st ( F is closed & A /\ F = D ) let D be Subset of Y; ::_thesis: ( D c= A implies ex F being Subset of Y st ( F is closed & A /\ F = D ) ) A \ D c= A by XBOOLE_1:36; then consider G being Subset of Y such that A2: G is open and A3: A /\ G = A \ D by A1, Def3; assume A4: D c= A ; ::_thesis: ex F being Subset of Y st ( F is closed & A /\ F = D ) now__::_thesis:_ex_F_being_Element_of_bool_the_carrier_of_Y_st_ (_F_is_closed_&_A_/\_F_=_D_) take F = ([#] Y) \ G; ::_thesis: ( F is closed & A /\ F = D ) G = ([#] Y) \ F by PRE_TOPC:3; hence F is closed by A2, PRE_TOPC:def_3; ::_thesis: A /\ F = D A /\ ([#] Y) = A by XBOOLE_1:28; then A /\ F = A \ G by XBOOLE_1:49; then A /\ F = A \ (A \ D) by A3, XBOOLE_1:47; then A /\ F = A /\ D by XBOOLE_1:48; hence A /\ F = D by A4, XBOOLE_1:28; ::_thesis: verum end; hence ex F being Subset of Y st ( F is closed & A /\ F = D ) ; ::_thesis: verum end; hereby ::_thesis: verum assume A5: for D being Subset of Y st D c= A holds ex F being Subset of Y st ( F is closed & A /\ F = D ) ; ::_thesis: A is discrete now__::_thesis:_for_D_being_Subset_of_Y_st_D_c=_A_holds_ ex_G_being_Subset_of_Y_st_ (_G_is_open_&_A_/\_G_=_D_) let D be Subset of Y; ::_thesis: ( D c= A implies ex G being Subset of Y st ( G is open & A /\ G = D ) ) consider F being Subset of Y such that A6: F is closed and A7: A /\ F = A \ D by A5, XBOOLE_1:36; assume A8: D c= A ; ::_thesis: ex G being Subset of Y st ( G is open & A /\ G = D ) now__::_thesis:_ex_G_being_Element_of_bool_the_carrier_of_Y_st_ (_G_is_open_&_A_/\_G_=_D_) take G = ([#] Y) \ F; ::_thesis: ( G is open & A /\ G = D ) thus G is open by A6, PRE_TOPC:def_3; ::_thesis: A /\ G = D A /\ ([#] Y) = A by XBOOLE_1:28; then A /\ G = A \ F by XBOOLE_1:49; then A /\ G = A \ (A \ D) by A7, XBOOLE_1:47; then A /\ G = A /\ D by XBOOLE_1:48; hence A /\ G = D by A8, XBOOLE_1:28; ::_thesis: verum end; hence ex G being Subset of Y st ( G is open & A /\ G = D ) ; ::_thesis: verum end; hence A is discrete by Def3; ::_thesis: verum end; end; end; :: deftheorem Def4 defines discrete TEX_2:def_4_:_ for Y being TopStruct for A being Subset of Y holds ( A is discrete iff for D being Subset of Y st D c= A holds ex F being Subset of Y st ( F is closed & A /\ F = D ) ); theorem Th19: :: TEX_2:19 for Y0, Y1 being TopStruct for D0 being Subset of Y0 for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is discrete holds D1 is discrete proof let Y0, Y1 be TopStruct ; ::_thesis: for D0 being Subset of Y0 for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is discrete holds D1 is discrete let D0 be Subset of Y0; ::_thesis: for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is discrete holds D1 is discrete let D1 be Subset of Y1; ::_thesis: ( TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is discrete implies D1 is discrete ) assume A1: TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) ; ::_thesis: ( not D0 = D1 or not D0 is discrete or D1 is discrete ) assume A2: D0 = D1 ; ::_thesis: ( not D0 is discrete or D1 is discrete ) assume A3: D0 is discrete ; ::_thesis: D1 is discrete now__::_thesis:_for_D_being_Subset_of_Y1_st_D_c=_D1_holds_ ex_G_being_Subset_of_Y1_st_ (_G_is_open_&_D1_/\_G_=_D_) let D be Subset of Y1; ::_thesis: ( D c= D1 implies ex G being Subset of Y1 st ( G is open & D1 /\ G = D ) ) reconsider E = D as Subset of Y0 by A1; assume D c= D1 ; ::_thesis: ex G being Subset of Y1 st ( G is open & D1 /\ G = D ) then consider G0 being Subset of Y0 such that A4: G0 is open and A5: D0 /\ G0 = E by A2, A3, Def3; reconsider G = G0 as Subset of Y1 by A1; now__::_thesis:_ex_G_being_Subset_of_Y1_st_ (_G_is_open_&_D1_/\_G_=_D_) take G = G; ::_thesis: ( G is open & D1 /\ G = D ) G in the topology of Y1 by A1, A4, PRE_TOPC:def_2; hence G is open by PRE_TOPC:def_2; ::_thesis: D1 /\ G = D thus D1 /\ G = D by A2, A5; ::_thesis: verum end; hence ex G being Subset of Y1 st ( G is open & D1 /\ G = D ) ; ::_thesis: verum end; hence D1 is discrete by Def3; ::_thesis: verum end; theorem Th20: :: TEX_2:20 for Y being non empty TopStruct for Y0 being non empty SubSpace of Y for A being Subset of Y st A = the carrier of Y0 holds ( A is discrete iff Y0 is discrete ) proof let Y be non empty TopStruct ; ::_thesis: for Y0 being non empty SubSpace of Y for A being Subset of Y st A = the carrier of Y0 holds ( A is discrete iff Y0 is discrete ) let Y0 be non empty SubSpace of Y; ::_thesis: for A being Subset of Y st A = the carrier of Y0 holds ( A is discrete iff Y0 is discrete ) let A be Subset of Y; ::_thesis: ( A = the carrier of Y0 implies ( A is discrete iff Y0 is discrete ) ) assume A1: A = the carrier of Y0 ; ::_thesis: ( A is discrete iff Y0 is discrete ) A2: [#] Y = the carrier of Y ; [#] Y0 = the carrier of Y0 ; then A3: the carrier of Y0 c= the carrier of Y by A2, PRE_TOPC:def_4; hereby ::_thesis: ( Y0 is discrete implies A is discrete ) assume A4: A is discrete ; ::_thesis: Y0 is discrete now__::_thesis:_for_C_being_set_st_C_in_bool_the_carrier_of_Y0_holds_ C_in_the_topology_of_Y0 let C be set ; ::_thesis: ( C in bool the carrier of Y0 implies C in the topology of Y0 ) assume C in bool the carrier of Y0 ; ::_thesis: C in the topology of Y0 then reconsider B = C as Subset of Y0 ; reconsider D = B as Subset of Y by A3, XBOOLE_1:1; consider G being Subset of Y such that A5: G is open and A6: A /\ G = D by A1, A4, Def3; now__::_thesis:_ex_G_being_Subset_of_Y_st_ (_G_in_the_topology_of_Y_&_B_=_G_/\_([#]_Y0)_) take G = G; ::_thesis: ( G in the topology of Y & B = G /\ ([#] Y0) ) thus G in the topology of Y by A5, PRE_TOPC:def_2; ::_thesis: B = G /\ ([#] Y0) thus B = G /\ ([#] Y0) by A1, A6; ::_thesis: verum end; hence C in the topology of Y0 by PRE_TOPC:def_4; ::_thesis: verum end; then bool the carrier of Y0 c= the topology of Y0 by TARSKI:def_3; then the topology of Y0 = bool the carrier of Y0 by XBOOLE_0:def_10; hence Y0 is discrete by TDLAT_3:def_1; ::_thesis: verum end; hereby ::_thesis: verum assume A7: Y0 is discrete ; ::_thesis: A is discrete now__::_thesis:_for_D_being_Subset_of_Y_st_D_c=_A_holds_ ex_G_being_Subset_of_Y_st_ (_G_is_open_&_A_/\_G_=_D_) let D be Subset of Y; ::_thesis: ( D c= A implies ex G being Subset of Y st ( G is open & A /\ G = D ) ) assume D c= A ; ::_thesis: ex G being Subset of Y st ( G is open & A /\ G = D ) then reconsider B = D as Subset of Y0 by A1; B is open by A7, TDLAT_3:15; then B in the topology of Y0 by PRE_TOPC:def_2; then consider G being Subset of Y such that A8: G in the topology of Y and A9: B = G /\ ([#] Y0) by PRE_TOPC:def_4; reconsider G = G as Subset of Y ; take G = G; ::_thesis: ( G is open & A /\ G = D ) thus G is open by A8, PRE_TOPC:def_2; ::_thesis: A /\ G = D thus A /\ G = D by A1, A9; ::_thesis: verum end; hence A is discrete by Def3; ::_thesis: verum end; end; theorem Th21: :: TEX_2:21 for Y being non empty TopStruct for A being Subset of Y st A = the carrier of Y holds ( A is discrete iff Y is discrete ) proof let Y be non empty TopStruct ; ::_thesis: for A being Subset of Y st A = the carrier of Y holds ( A is discrete iff Y is discrete ) let A be Subset of Y; ::_thesis: ( A = the carrier of Y implies ( A is discrete iff Y is discrete ) ) assume A1: A = the carrier of Y ; ::_thesis: ( A is discrete iff Y is discrete ) hereby ::_thesis: ( Y is discrete implies A is discrete ) assume A2: A is discrete ; ::_thesis: Y is discrete now__::_thesis:_for_C_being_set_st_C_in_bool_the_carrier_of_Y_holds_ C_in_the_topology_of_Y let C be set ; ::_thesis: ( C in bool the carrier of Y implies C in the topology of Y ) assume C in bool the carrier of Y ; ::_thesis: C in the topology of Y then reconsider B = C as Subset of Y ; consider G being Subset of Y such that A3: G is open and A4: A /\ G = B by A1, A2, Def3; G = B by A1, A4, XBOOLE_1:28; hence C in the topology of Y by A3, PRE_TOPC:def_2; ::_thesis: verum end; then bool the carrier of Y c= the topology of Y by TARSKI:def_3; then the topology of Y = bool the carrier of Y by XBOOLE_0:def_10; hence Y is discrete by TDLAT_3:def_1; ::_thesis: verum end; hereby ::_thesis: verum assume Y is discrete ; ::_thesis: A is discrete then reconsider Y = Y as non empty discrete TopStruct ; now__::_thesis:_for_D_being_Subset_of_Y_st_D_c=_A_holds_ ex_G_being_Subset_of_Y_st_ (_G_is_open_&_A_/\_G_=_D_) let D be Subset of Y; ::_thesis: ( D c= A implies ex G being Subset of Y st ( G is open & A /\ G = D ) ) assume A5: D c= A ; ::_thesis: ex G being Subset of Y st ( G is open & A /\ G = D ) reconsider G = D as Subset of Y ; take G = G; ::_thesis: ( G is open & A /\ G = D ) thus G is open by TDLAT_3:15; ::_thesis: A /\ G = D thus A /\ G = D by A5, XBOOLE_1:28; ::_thesis: verum end; hence A is discrete by Def3; ::_thesis: verum end; end; theorem Th22: :: TEX_2:22 for Y being TopStruct for A, B being Subset of Y st B c= A & A is discrete holds B is discrete proof let Y be TopStruct ; ::_thesis: for A, B being Subset of Y st B c= A & A is discrete holds B is discrete let A, B be Subset of Y; ::_thesis: ( B c= A & A is discrete implies B is discrete ) assume A1: B c= A ; ::_thesis: ( not A is discrete or B is discrete ) assume A2: A is discrete ; ::_thesis: B is discrete now__::_thesis:_for_D_being_Subset_of_Y_st_D_c=_B_holds_ ex_G_being_Subset_of_Y_st_ (_G_is_open_&_B_/\_G_=_D_) let D be Subset of Y; ::_thesis: ( D c= B implies ex G being Subset of Y st ( G is open & B /\ G = D ) ) assume A3: D c= B ; ::_thesis: ex G being Subset of Y st ( G is open & B /\ G = D ) then D c= A by A1, XBOOLE_1:1; then consider G being Subset of Y such that A4: G is open and A5: A /\ G = D by A2, Def3; hereby ::_thesis: verum take G = G; ::_thesis: ( G is open & B /\ G = D ) D c= G by A5, XBOOLE_1:17; then A6: D c= B /\ G by A3, XBOOLE_1:19; B /\ G c= A /\ G by A1, XBOOLE_1:26; hence ( G is open & B /\ G = D ) by A4, A5, A6, XBOOLE_0:def_10; ::_thesis: verum end; end; hence B is discrete by Def3; ::_thesis: verum end; theorem :: TEX_2:23 for Y being TopStruct for A, B being Subset of Y st ( A is discrete or B is discrete ) holds A /\ B is discrete proof let Y be TopStruct ; ::_thesis: for A, B being Subset of Y st ( A is discrete or B is discrete ) holds A /\ B is discrete let A, B be Subset of Y; ::_thesis: ( ( A is discrete or B is discrete ) implies A /\ B is discrete ) assume A1: ( A is discrete or B is discrete ) ; ::_thesis: A /\ B is discrete hereby ::_thesis: verum percases ( A is discrete or B is discrete ) by A1; suppose A is discrete ; ::_thesis: A /\ B is discrete hence A /\ B is discrete by Th22, XBOOLE_1:17; ::_thesis: verum end; suppose B is discrete ; ::_thesis: A /\ B is discrete hence A /\ B is discrete by Th22, XBOOLE_1:17; ::_thesis: verum end; end; end; end; theorem Th24: :: TEX_2:24 for Y being TopStruct st ( for P, Q being Subset of Y st P is open & Q is open holds ( P /\ Q is open & P \/ Q is open ) ) holds for A, B being Subset of Y st A is open & B is open & A is discrete & B is discrete holds A \/ B is discrete proof let Y be TopStruct ; ::_thesis: ( ( for P, Q being Subset of Y st P is open & Q is open holds ( P /\ Q is open & P \/ Q is open ) ) implies for A, B being Subset of Y st A is open & B is open & A is discrete & B is discrete holds A \/ B is discrete ) assume A1: for P, Q being Subset of Y st P is open & Q is open holds ( P /\ Q is open & P \/ Q is open ) ; ::_thesis: for A, B being Subset of Y st A is open & B is open & A is discrete & B is discrete holds A \/ B is discrete let A, B be Subset of Y; ::_thesis: ( A is open & B is open & A is discrete & B is discrete implies A \/ B is discrete ) assume that A2: A is open and A3: B is open ; ::_thesis: ( not A is discrete or not B is discrete or A \/ B is discrete ) assume that A4: A is discrete and A5: B is discrete ; ::_thesis: A \/ B is discrete now__::_thesis:_for_D_being_Subset_of_Y_st_D_c=_A_\/_B_holds_ ex_G_being_Subset_of_Y_st_ (_G_is_open_&_(A_\/_B)_/\_G_=_D_) let D be Subset of Y; ::_thesis: ( D c= A \/ B implies ex G being Subset of Y st ( G is open & (A \/ B) /\ G = D ) ) D /\ A c= A by XBOOLE_1:17; then consider G1 being Subset of Y such that A6: G1 is open and A7: A /\ G1 = D /\ A by A4, Def3; D /\ B c= B by XBOOLE_1:17; then consider G2 being Subset of Y such that A8: G2 is open and A9: B /\ G2 = D /\ B by A5, Def3; assume D c= A \/ B ; ::_thesis: ex G being Subset of Y st ( G is open & (A \/ B) /\ G = D ) then A10: D = D /\ (A \/ B) by XBOOLE_1:28; now__::_thesis:_ex_G_being_Element_of_bool_the_carrier_of_Y_st_ (_G_is_open_&_(A_\/_B)_/\_G_=_D_) take G = (A /\ G1) \/ (B /\ G2); ::_thesis: ( G is open & (A \/ B) /\ G = D ) A11: B /\ G2 is open by A1, A3, A8; A /\ G1 is open by A1, A2, A6; hence G is open by A1, A11; ::_thesis: (A \/ B) /\ G = D thus (A \/ B) /\ G = D by A10, A7, A9, XBOOLE_1:23; ::_thesis: verum end; hence ex G being Subset of Y st ( G is open & (A \/ B) /\ G = D ) ; ::_thesis: verum end; hence A \/ B is discrete by Def3; ::_thesis: verum end; theorem Th25: :: TEX_2:25 for Y being TopStruct st ( for P, Q being Subset of Y st P is closed & Q is closed holds ( P /\ Q is closed & P \/ Q is closed ) ) holds for A, B being Subset of Y st A is closed & B is closed & A is discrete & B is discrete holds A \/ B is discrete proof let Y be TopStruct ; ::_thesis: ( ( for P, Q being Subset of Y st P is closed & Q is closed holds ( P /\ Q is closed & P \/ Q is closed ) ) implies for A, B being Subset of Y st A is closed & B is closed & A is discrete & B is discrete holds A \/ B is discrete ) assume A1: for P, Q being Subset of Y st P is closed & Q is closed holds ( P /\ Q is closed & P \/ Q is closed ) ; ::_thesis: for A, B being Subset of Y st A is closed & B is closed & A is discrete & B is discrete holds A \/ B is discrete let A, B be Subset of Y; ::_thesis: ( A is closed & B is closed & A is discrete & B is discrete implies A \/ B is discrete ) assume that A2: A is closed and A3: B is closed ; ::_thesis: ( not A is discrete or not B is discrete or A \/ B is discrete ) assume that A4: A is discrete and A5: B is discrete ; ::_thesis: A \/ B is discrete now__::_thesis:_for_D_being_Subset_of_Y_st_D_c=_A_\/_B_holds_ ex_F_being_Subset_of_Y_st_ (_F_is_closed_&_(A_\/_B)_/\_F_=_D_) let D be Subset of Y; ::_thesis: ( D c= A \/ B implies ex F being Subset of Y st ( F is closed & (A \/ B) /\ F = D ) ) D /\ A c= A by XBOOLE_1:17; then consider F1 being Subset of Y such that A6: F1 is closed and A7: A /\ F1 = D /\ A by A4, Def4; D /\ B c= B by XBOOLE_1:17; then consider F2 being Subset of Y such that A8: F2 is closed and A9: B /\ F2 = D /\ B by A5, Def4; assume D c= A \/ B ; ::_thesis: ex F being Subset of Y st ( F is closed & (A \/ B) /\ F = D ) then A10: D = D /\ (A \/ B) by XBOOLE_1:28; now__::_thesis:_ex_F_being_Element_of_bool_the_carrier_of_Y_st_ (_F_is_closed_&_(A_\/_B)_/\_F_=_D_) take F = (A /\ F1) \/ (B /\ F2); ::_thesis: ( F is closed & (A \/ B) /\ F = D ) A11: B /\ F2 is closed by A1, A3, A8; A /\ F1 is closed by A1, A2, A6; hence F is closed by A1, A11; ::_thesis: (A \/ B) /\ F = D thus (A \/ B) /\ F = D by A10, A7, A9, XBOOLE_1:23; ::_thesis: verum end; hence ex F being Subset of Y st ( F is closed & (A \/ B) /\ F = D ) ; ::_thesis: verum end; hence A \/ B is discrete by Def4; ::_thesis: verum end; theorem Th26: :: TEX_2:26 for Y being TopStruct for A being Subset of Y st A is discrete holds for x being Point of Y st x in A holds ex G being Subset of Y st ( G is open & A /\ G = {x} ) proof let Y be TopStruct ; ::_thesis: for A being Subset of Y st A is discrete holds for x being Point of Y st x in A holds ex G being Subset of Y st ( G is open & A /\ G = {x} ) let A be Subset of Y; ::_thesis: ( A is discrete implies for x being Point of Y st x in A holds ex G being Subset of Y st ( G is open & A /\ G = {x} ) ) assume A1: A is discrete ; ::_thesis: for x being Point of Y st x in A holds ex G being Subset of Y st ( G is open & A /\ G = {x} ) let x be Point of Y; ::_thesis: ( x in A implies ex G being Subset of Y st ( G is open & A /\ G = {x} ) ) assume A2: x in A ; ::_thesis: ex G being Subset of Y st ( G is open & A /\ G = {x} ) then reconsider Y9 = Y as non empty TopStruct ; reconsider B = {x} as Subset of Y9 by ZFMISC_1:31; reconsider A9 = A as Subset of Y9 ; {x} c= A9 by A2, ZFMISC_1:31; then consider G being Subset of Y9 such that A3: G is open and A4: A9 /\ G = B by A1, Def3; reconsider G = G as Subset of Y ; take G ; ::_thesis: ( G is open & A /\ G = {x} ) thus ( G is open & A /\ G = {x} ) by A3, A4; ::_thesis: verum end; theorem :: TEX_2:27 for Y being TopStruct for A being Subset of Y st A is discrete holds for x being Point of Y st x in A holds ex F being Subset of Y st ( F is closed & A /\ F = {x} ) proof let Y be TopStruct ; ::_thesis: for A being Subset of Y st A is discrete holds for x being Point of Y st x in A holds ex F being Subset of Y st ( F is closed & A /\ F = {x} ) let A be Subset of Y; ::_thesis: ( A is discrete implies for x being Point of Y st x in A holds ex F being Subset of Y st ( F is closed & A /\ F = {x} ) ) assume A1: A is discrete ; ::_thesis: for x being Point of Y st x in A holds ex F being Subset of Y st ( F is closed & A /\ F = {x} ) let x be Point of Y; ::_thesis: ( x in A implies ex F being Subset of Y st ( F is closed & A /\ F = {x} ) ) assume A2: x in A ; ::_thesis: ex F being Subset of Y st ( F is closed & A /\ F = {x} ) then reconsider Y9 = Y as non empty TopStruct ; reconsider B = {x} as Subset of Y9 by ZFMISC_1:31; reconsider A9 = A as Subset of Y9 ; {x} c= A9 by A2, ZFMISC_1:31; then consider F being Subset of Y such that A3: F is closed and A4: A9 /\ F = B by A1, Def4; take F ; ::_thesis: ( F is closed & A /\ F = {x} ) thus ( F is closed & A /\ F = {x} ) by A3, A4; ::_thesis: verum end; theorem Th28: :: TEX_2:28 for X being non empty TopSpace for A0 being non empty Subset of X st A0 is discrete holds ex X0 being non empty strict discrete SubSpace of X st A0 = the carrier of X0 proof let X be non empty TopSpace; ::_thesis: for A0 being non empty Subset of X st A0 is discrete holds ex X0 being non empty strict discrete SubSpace of X st A0 = the carrier of X0 let A0 be non empty Subset of X; ::_thesis: ( A0 is discrete implies ex X0 being non empty strict discrete SubSpace of X st A0 = the carrier of X0 ) consider X0 being non empty strict SubSpace of X such that A1: A0 = the carrier of X0 by TSEP_1:10; assume A0 is discrete ; ::_thesis: ex X0 being non empty strict discrete SubSpace of X st A0 = the carrier of X0 then reconsider X0 = X0 as non empty strict discrete SubSpace of X by A1, Th20; take X0 ; ::_thesis: A0 = the carrier of X0 thus A0 = the carrier of X0 by A1; ::_thesis: verum end; theorem Th29: :: TEX_2:29 for X being non empty TopSpace for A being empty Subset of X holds A is discrete proof let X be non empty TopSpace; ::_thesis: for A being empty Subset of X holds A is discrete let A be empty Subset of X; ::_thesis: A is discrete now__::_thesis:_for_D_being_Subset_of_X_st_D_c=_A_holds_ ex_G_being_Subset_of_X_st_ (_G_is_open_&_A_/\_G_=_D_) let D be Subset of X; ::_thesis: ( D c= A implies ex G being Subset of X st ( G is open & A /\ G = D ) ) assume A1: D c= A ; ::_thesis: ex G being Subset of X st ( G is open & A /\ G = D ) now__::_thesis:_ex_G_being_Element_of_bool_the_carrier_of_X_st_ (_G_is_open_&_A_/\_G_=_D_) take G = {} X; ::_thesis: ( G is open & A /\ G = D ) thus ( G is open & A /\ G = D ) by A1; ::_thesis: verum end; hence ex G being Subset of X st ( G is open & A /\ G = D ) ; ::_thesis: verum end; hence A is discrete by Def3; ::_thesis: verum end; theorem Th30: :: TEX_2:30 for X being non empty TopSpace for x being Point of X holds {x} is discrete proof let X be non empty TopSpace; ::_thesis: for x being Point of X holds {x} is discrete let x be Point of X; ::_thesis: {x} is discrete now__::_thesis:_for_D_being_Subset_of_X_st_D_c=_{x}_holds_ ex_G_being_Subset_of_X_st_ (_G_is_open_&_{x}_/\_G_=_D_) let D be Subset of X; ::_thesis: ( D c= {x} implies ex G being Subset of X st ( G is open & {x} /\ G = D ) ) A1: now__::_thesis:_(_D_=_{}_implies_ex_G_being_Element_of_bool_the_carrier_of_X_st_ (_G_is_open_&_{x}_/\_G_=_D_)_) assume A2: D = {} ; ::_thesis: ex G being Element of bool the carrier of X st ( G is open & {x} /\ G = D ) hereby ::_thesis: verum take G = {} X; ::_thesis: ( G is open & {x} /\ G = D ) thus ( G is open & {x} /\ G = D ) by A2; ::_thesis: verum end; end; A3: now__::_thesis:_(_D_=_{x}_implies_ex_G_being_Element_of_bool_the_carrier_of_X_st_ (_G_is_open_&_{x}_/\_G_=_D_)_) assume A4: D = {x} ; ::_thesis: ex G being Element of bool the carrier of X st ( G is open & {x} /\ G = D ) hereby ::_thesis: verum take G = [#] X; ::_thesis: ( G is open & {x} /\ G = D ) thus ( G is open & {x} /\ G = D ) by A4, XBOOLE_1:28; ::_thesis: verum end; end; assume D c= {x} ; ::_thesis: ex G being Subset of X st ( G is open & {x} /\ G = D ) hence ex G being Subset of X st ( G is open & {x} /\ G = D ) by A1, A3, ZFMISC_1:33; ::_thesis: verum end; hence {x} is discrete by Def3; ::_thesis: verum end; theorem Th31: :: TEX_2:31 for X being non empty TopSpace for A being Subset of X st ( for x being Point of X st x in A holds ex G being Subset of X st ( G is open & A /\ G = {x} ) ) holds A is discrete proof let X be non empty TopSpace; ::_thesis: for A being Subset of X st ( for x being Point of X st x in A holds ex G being Subset of X st ( G is open & A /\ G = {x} ) ) holds A is discrete let A be Subset of X; ::_thesis: ( ( for x being Point of X st x in A holds ex G being Subset of X st ( G is open & A /\ G = {x} ) ) implies A is discrete ) assume A1: for x being Point of X st x in A holds ex G being Subset of X st ( G is open & A /\ G = {x} ) ; ::_thesis: A is discrete hereby ::_thesis: verum percases ( A is empty or not A is empty ) ; suppose A is empty ; ::_thesis: A is discrete hence A is discrete by Th29; ::_thesis: verum end; suppose not A is empty ; ::_thesis: A is discrete then consider X0 being non empty strict SubSpace of X such that A2: A = the carrier of X0 by TSEP_1:10; A3: [#] X = the carrier of X ; [#] X0 = the carrier of X0 ; then A4: the carrier of X0 c= the carrier of X by A3, PRE_TOPC:def_4; now__::_thesis:_for_C_being_Subset_of_X0 for_y_being_Point_of_X0_st_C_=_{y}_holds_ C_is_open let C be Subset of X0; ::_thesis: for y being Point of X0 st C = {y} holds C is open let y be Point of X0; ::_thesis: ( C = {y} implies C is open ) reconsider x = y as Point of X by A4, TARSKI:def_3; consider G being Subset of X such that A5: G is open and A6: A /\ G = {x} by A1, A2; assume A7: C = {y} ; ::_thesis: C is open now__::_thesis:_ex_G_being_Subset_of_X_st_ (_G_in_the_topology_of_X_&_G_/\_([#]_X0)_=_C_) take G = G; ::_thesis: ( G in the topology of X & G /\ ([#] X0) = C ) thus G in the topology of X by A5, PRE_TOPC:def_2; ::_thesis: G /\ ([#] X0) = C thus G /\ ([#] X0) = C by A2, A7, A6; ::_thesis: verum end; then C in the topology of X0 by PRE_TOPC:def_4; hence C is open by PRE_TOPC:def_2; ::_thesis: verum end; then X0 is discrete by TDLAT_3:17; hence A is discrete by A2, Th20; ::_thesis: verum end; end; end; end; theorem :: TEX_2:32 for X being non empty TopSpace for A, B being Subset of X st A is open & B is open & A is discrete & B is discrete holds A \/ B is discrete proof let X be non empty TopSpace; ::_thesis: for A, B being Subset of X st A is open & B is open & A is discrete & B is discrete holds A \/ B is discrete let A, B be Subset of X; ::_thesis: ( A is open & B is open & A is discrete & B is discrete implies A \/ B is discrete ) assume that A1: A is open and A2: B is open ; ::_thesis: ( not A is discrete or not B is discrete or A \/ B is discrete ) assume that A3: A is discrete and A4: B is discrete ; ::_thesis: A \/ B is discrete for P, Q being Subset of X st P is open & Q is open holds ( P /\ Q is open & P \/ Q is open ) ; hence A \/ B is discrete by A1, A2, A3, A4, Th24; ::_thesis: verum end; theorem :: TEX_2:33 for X being non empty TopSpace for A, B being Subset of X st A is closed & B is closed & A is discrete & B is discrete holds A \/ B is discrete proof let X be non empty TopSpace; ::_thesis: for A, B being Subset of X st A is closed & B is closed & A is discrete & B is discrete holds A \/ B is discrete let A, B be Subset of X; ::_thesis: ( A is closed & B is closed & A is discrete & B is discrete implies A \/ B is discrete ) assume that A1: A is closed and A2: B is closed ; ::_thesis: ( not A is discrete or not B is discrete or A \/ B is discrete ) assume that A3: A is discrete and A4: B is discrete ; ::_thesis: A \/ B is discrete for P, Q being Subset of X st P is closed & Q is closed holds ( P /\ Q is closed & P \/ Q is closed ) ; hence A \/ B is discrete by A1, A2, A3, A4, Th25; ::_thesis: verum end; Lm3: for P, Q being set st P c= Q & P <> Q holds Q \ P <> {} proof let P, Q be set ; ::_thesis: ( P c= Q & P <> Q implies Q \ P <> {} ) assume P c= Q ; ::_thesis: ( not P <> Q or Q \ P <> {} ) then A1: Q = P \/ (Q \ P) by XBOOLE_1:45; assume A2: P <> Q ; ::_thesis: Q \ P <> {} assume Q \ P = {} ; ::_thesis: contradiction hence contradiction by A1, A2; ::_thesis: verum end; theorem :: TEX_2:34 for X being non empty TopSpace for A being Subset of X st A is everywhere_dense & A is discrete holds A is open proof let X be non empty TopSpace; ::_thesis: for A being Subset of X st A is everywhere_dense & A is discrete holds A is open let A be Subset of X; ::_thesis: ( A is everywhere_dense & A is discrete implies A is open ) assume A is everywhere_dense ; ::_thesis: ( not A is discrete or A is open ) then A1: Cl (Int A) = the carrier of X by TOPS_3:def_5; assume A2: A is discrete ; ::_thesis: A is open assume not A is open ; ::_thesis: contradiction then A \ (Int A) <> {} by Lm3, TOPS_1:16; then consider a being set such that A3: a in A \ (Int A) by XBOOLE_0:def_1; reconsider a = a as Point of X by A3; A \ (Int A) c= A by XBOOLE_1:36; then consider G being Subset of X such that A4: G is open and A5: A /\ G = {a} by A2, A3, Th26; A6: now__::_thesis:_not_(Int_A)_/\_G_=_{a} assume (Int A) /\ G = {a} ; ::_thesis: contradiction then {a} c= Int A by XBOOLE_1:17; then a in Int A by ZFMISC_1:31; hence contradiction by A3, XBOOLE_0:def_5; ::_thesis: verum end; (Int A) /\ G c= {a} by A5, TOPS_1:16, XBOOLE_1:26; then ( (Int A) /\ G = {} or (Int A) /\ G = {a} ) by ZFMISC_1:33; then ( Int A misses G or (Int A) /\ G = {a} ) by XBOOLE_0:def_7; then Cl (Int A) misses G by A4, A6, TSEP_1:36; then A7: (Cl (Int A)) /\ G = {} by XBOOLE_0:def_7; {a} c= G by A5, XBOOLE_1:17; hence contradiction by A1, A7, XBOOLE_1:3, XBOOLE_1:19; ::_thesis: verum end; theorem Th35: :: TEX_2:35 for X being non empty TopSpace for A being Subset of X holds ( A is discrete iff for D being Subset of X st D c= A holds A /\ (Cl D) = D ) proof let X be non empty TopSpace; ::_thesis: for A being Subset of X holds ( A is discrete iff for D being Subset of X st D c= A holds A /\ (Cl D) = D ) let A be Subset of X; ::_thesis: ( A is discrete iff for D being Subset of X st D c= A holds A /\ (Cl D) = D ) thus ( A is discrete implies for D being Subset of X st D c= A holds A /\ (Cl D) = D ) ::_thesis: ( ( for D being Subset of X st D c= A holds A /\ (Cl D) = D ) implies A is discrete ) proof assume A1: A is discrete ; ::_thesis: for D being Subset of X st D c= A holds A /\ (Cl D) = D let D be Subset of X; ::_thesis: ( D c= A implies A /\ (Cl D) = D ) assume A2: D c= A ; ::_thesis: A /\ (Cl D) = D then consider F being Subset of X such that A3: F is closed and A4: A /\ F = D by A1, Def4; Cl D c= F by A3, A4, TOPS_1:5, XBOOLE_1:17; then A5: A /\ (Cl D) c= D by A4, XBOOLE_1:26; D c= Cl D by PRE_TOPC:18; then D c= A /\ (Cl D) by A2, XBOOLE_1:19; hence A /\ (Cl D) = D by A5, XBOOLE_0:def_10; ::_thesis: verum end; assume A6: for D being Subset of X st D c= A holds A /\ (Cl D) = D ; ::_thesis: A is discrete now__::_thesis:_for_D_being_Subset_of_X_st_D_c=_A_holds_ ex_F_being_Subset_of_X_st_ (_F_is_closed_&_A_/\_F_=_D_) let D be Subset of X; ::_thesis: ( D c= A implies ex F being Subset of X st ( F is closed & A /\ F = D ) ) assume A7: D c= A ; ::_thesis: ex F being Subset of X st ( F is closed & A /\ F = D ) now__::_thesis:_ex_F_being_Element_of_bool_the_carrier_of_X_st_ (_F_is_closed_&_A_/\_F_=_D_) take F = Cl D; ::_thesis: ( F is closed & A /\ F = D ) thus F is closed ; ::_thesis: A /\ F = D thus A /\ F = D by A6, A7; ::_thesis: verum end; hence ex F being Subset of X st ( F is closed & A /\ F = D ) ; ::_thesis: verum end; hence A is discrete by Def4; ::_thesis: verum end; theorem Th36: :: TEX_2:36 for X being non empty TopSpace for A being Subset of X st A is discrete holds for x being Point of X st x in A holds A /\ (Cl {x}) = {x} proof let X be non empty TopSpace; ::_thesis: for A being Subset of X st A is discrete holds for x being Point of X st x in A holds A /\ (Cl {x}) = {x} let A be Subset of X; ::_thesis: ( A is discrete implies for x being Point of X st x in A holds A /\ (Cl {x}) = {x} ) assume A1: A is discrete ; ::_thesis: for x being Point of X st x in A holds A /\ (Cl {x}) = {x} let x be Point of X; ::_thesis: ( x in A implies A /\ (Cl {x}) = {x} ) assume x in A ; ::_thesis: A /\ (Cl {x}) = {x} then {x} c= A by ZFMISC_1:31; hence A /\ (Cl {x}) = {x} by A1, Th35; ::_thesis: verum end; theorem :: TEX_2:37 for X being non empty discrete TopSpace for A being Subset of X holds A is discrete proof let X be non empty discrete TopSpace; ::_thesis: for A being Subset of X holds A is discrete let A be Subset of X; ::_thesis: A is discrete hereby ::_thesis: verum percases ( A is empty or not A is empty ) ; suppose A is empty ; ::_thesis: A is discrete hence A is discrete by Th29; ::_thesis: verum end; suppose not A is empty ; ::_thesis: A is discrete then ex X0 being non empty strict SubSpace of X st A = the carrier of X0 by TSEP_1:10; hence A is discrete by Th20; ::_thesis: verum end; end; end; end; theorem Th38: :: TEX_2:38 for X being non empty anti-discrete TopSpace for A being non empty Subset of X holds ( A is discrete iff A is trivial ) proof let X be non empty anti-discrete TopSpace; ::_thesis: for A being non empty Subset of X holds ( A is discrete iff A is trivial ) let A be non empty Subset of X; ::_thesis: ( A is discrete iff A is trivial ) hereby ::_thesis: ( A is trivial implies A is discrete ) consider a being set such that A1: a in A by XBOOLE_0:def_1; reconsider a = a as Point of X by A1; assume A is discrete ; ::_thesis: A is trivial then consider G being Subset of X such that A2: G is open and A3: A /\ G = {a} by A1, Th26; G <> {} by A3; then A4: G = the carrier of X by A2, TDLAT_3:18; now__::_thesis:_ex_a_being_Point_of_X_st_A_=_{a} take a = a; ::_thesis: A = {a} thus A = {a} by A3, A4, XBOOLE_1:28; ::_thesis: verum end; hence A is trivial ; ::_thesis: verum end; hereby ::_thesis: verum assume A is trivial ; ::_thesis: A is discrete then ex a being Element of A st A = {a} by SUBSET_1:46; hence A is discrete by Th30; ::_thesis: verum end; end; definition let Y be TopStruct ; let IT be Subset of Y; attrIT is maximal_discrete means :Def5: :: TEX_2:def 5 ( IT is discrete & ( for D being Subset of Y st D is discrete & IT c= D holds IT = D ) ); end; :: deftheorem Def5 defines maximal_discrete TEX_2:def_5_:_ for Y being TopStruct for IT being Subset of Y holds ( IT is maximal_discrete iff ( IT is discrete & ( for D being Subset of Y st D is discrete & IT c= D holds IT = D ) ) ); theorem :: TEX_2:39 for Y0, Y1 being TopStruct for D0 being Subset of Y0 for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is maximal_discrete holds D1 is maximal_discrete proof let Y0, Y1 be TopStruct ; ::_thesis: for D0 being Subset of Y0 for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is maximal_discrete holds D1 is maximal_discrete let D0 be Subset of Y0; ::_thesis: for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is maximal_discrete holds D1 is maximal_discrete let D1 be Subset of Y1; ::_thesis: ( TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & D0 = D1 & D0 is maximal_discrete implies D1 is maximal_discrete ) assume A1: TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) ; ::_thesis: ( not D0 = D1 or not D0 is maximal_discrete or D1 is maximal_discrete ) assume A2: D0 = D1 ; ::_thesis: ( not D0 is maximal_discrete or D1 is maximal_discrete ) assume A3: D0 is maximal_discrete ; ::_thesis: D1 is maximal_discrete A4: now__::_thesis:_for_D_being_Subset_of_Y1_st_D_is_discrete_&_D1_c=_D_holds_ D1_=_D let D be Subset of Y1; ::_thesis: ( D is discrete & D1 c= D implies D1 = D ) reconsider E = D as Subset of Y0 by A1; assume D is discrete ; ::_thesis: ( D1 c= D implies D1 = D ) then A5: E is discrete by A1, Th19; assume D1 c= D ; ::_thesis: D1 = D hence D1 = D by A2, A3, A5, Def5; ::_thesis: verum end; D0 is discrete by A3, Def5; then D1 is discrete by A1, A2, Th19; hence D1 is maximal_discrete by A4, Def5; ::_thesis: verum end; theorem Th40: :: TEX_2:40 for X being non empty TopSpace for A being empty Subset of X holds not A is maximal_discrete proof let X be non empty TopSpace; ::_thesis: for A being empty Subset of X holds not A is maximal_discrete consider a being set such that A1: a in the carrier of X by XBOOLE_0:def_1; reconsider a = a as Point of X by A1; let A be empty Subset of X; ::_thesis: not A is maximal_discrete now__::_thesis:_ex_C_being_Element_of_bool_the_carrier_of_X_st_ (_C_is_discrete_&_A_c=_C_&_A_<>_C_) take C = {a}; ::_thesis: ( C is discrete & A c= C & A <> C ) thus ( C is discrete & A c= C & A <> C ) by Th30, XBOOLE_1:2; ::_thesis: verum end; hence not A is maximal_discrete by Def5; ::_thesis: verum end; theorem Th41: :: TEX_2:41 for X being non empty TopSpace for A being Subset of X st A is open & A is maximal_discrete holds A is dense proof let X be non empty TopSpace; ::_thesis: for A being Subset of X st A is open & A is maximal_discrete holds A is dense let A be Subset of X; ::_thesis: ( A is open & A is maximal_discrete implies A is dense ) assume A1: A is open ; ::_thesis: ( not A is maximal_discrete or A is dense ) assume A2: A is maximal_discrete ; ::_thesis: A is dense then A3: A is discrete by Def5; assume not A is dense ; ::_thesis: contradiction then Cl A <> the carrier of X by TOPS_3:def_2; then the carrier of X \ (Cl A) <> {} by Lm3; then consider a being set such that A4: a in the carrier of X \ (Cl A) by XBOOLE_0:def_1; reconsider a = a as Point of X by A4; set B = A \/ {a}; A5: A c= A \/ {a} by XBOOLE_1:7; A6: now__::_thesis:_for_x_being_Point_of_X_st_x_in_A_\/_{a}_holds_ ex_G_being_Subset_of_X_st_ (_G_is_open_&_(A_\/_{a})_/\_G_=_{x}_) let x be Point of X; ::_thesis: ( x in A \/ {a} implies ex G being Subset of X st ( G is open & (A \/ {a}) /\ G = {x} ) ) assume x in A \/ {a} ; ::_thesis: ex G being Subset of X st ( G is open & (A \/ {a}) /\ G = {x} ) then A7: ( x in A or x in {a} ) by XBOOLE_0:def_3; now__::_thesis:_ex_E_being_Subset_of_X_st_ (_E_is_open_&_(A_\/_{a})_/\_E_=_{x}_) percases ( x in A or x = a ) by A7, TARSKI:def_1; supposeA8: x in A ; ::_thesis: ex E being Subset of X st ( E is open & (A \/ {a}) /\ E = {x} ) then A9: ex G being Subset of X st ( G is open & A /\ G = {x} ) by A3, Th26; now__::_thesis:_ex_E_being_Element_of_bool_the_carrier_of_X_st_ (_E_is_open_&_(A_\/_{a})_/\_E_=_{x}_) take E = {x}; ::_thesis: ( E is open & (A \/ {a}) /\ E = {x} ) thus E is open by A1, A9; ::_thesis: (A \/ {a}) /\ E = {x} {x} c= A \/ {a} by A5, A8, ZFMISC_1:31; hence (A \/ {a}) /\ E = {x} by XBOOLE_1:28; ::_thesis: verum end; hence ex E being Subset of X st ( E is open & (A \/ {a}) /\ E = {x} ) ; ::_thesis: verum end; supposeA10: x = a ; ::_thesis: ex G being Subset of X st ( G is open & (A \/ {a}) /\ G = {x} ) now__::_thesis:_ex_G_being_Element_of_bool_the_carrier_of_X_st_ (_G_is_open_&_(A_\/_{a})_/\_G_=_{x}_) take G = ([#] X) \ (Cl A); ::_thesis: ( G is open & (A \/ {a}) /\ G = {x} ) A11: (A \/ {a}) /\ G = (A /\ G) \/ ({a} /\ G) by XBOOLE_1:23; A12: G = (Cl A) ` ; hence G is open ; ::_thesis: (A \/ {a}) /\ G = {x} A c= Cl A by PRE_TOPC:18; then A misses G by A12, SUBSET_1:24; then A13: A /\ G = {} by XBOOLE_0:def_7; {a} c= G by A4, ZFMISC_1:31; hence (A \/ {a}) /\ G = {x} by A10, A13, A11, XBOOLE_1:28; ::_thesis: verum end; hence ex G being Subset of X st ( G is open & (A \/ {a}) /\ G = {x} ) ; ::_thesis: verum end; end; end; hence ex G being Subset of X st ( G is open & (A \/ {a}) /\ G = {x} ) ; ::_thesis: verum end; A c= Cl A by PRE_TOPC:18; then A14: not a in A by A4, XBOOLE_0:def_5; ex D being Subset of X st ( D is discrete & A c= D & A <> D ) proof take A \/ {a} ; ::_thesis: ( A \/ {a} is discrete & A c= A \/ {a} & A <> A \/ {a} ) thus A \/ {a} is discrete by A6, Th31; ::_thesis: ( A c= A \/ {a} & A <> A \/ {a} ) thus A c= A \/ {a} by XBOOLE_1:7; ::_thesis: A <> A \/ {a} now__::_thesis:_not_A_=_A_\/_{a} assume A = A \/ {a} ; ::_thesis: contradiction then {a} c= A by XBOOLE_1:7; hence contradiction by A14, ZFMISC_1:31; ::_thesis: verum end; hence A <> A \/ {a} ; ::_thesis: verum end; hence contradiction by A2, Def5; ::_thesis: verum end; theorem :: TEX_2:42 for X being non empty TopSpace for A being Subset of X st A is dense & A is discrete holds A is maximal_discrete proof let X be non empty TopSpace; ::_thesis: for A being Subset of X st A is dense & A is discrete holds A is maximal_discrete let A be Subset of X; ::_thesis: ( A is dense & A is discrete implies A is maximal_discrete ) assume A1: A is dense ; ::_thesis: ( not A is discrete or A is maximal_discrete ) assume A2: A is discrete ; ::_thesis: A is maximal_discrete assume not A is maximal_discrete ; ::_thesis: contradiction then consider D being Subset of X such that A3: D is discrete and A4: A c= D and A5: A <> D by A2, Def5; D \ A <> {} by A4, A5, Lm3; then consider a being set such that A6: a in D \ A by XBOOLE_0:def_1; reconsider a = a as Point of X by A6; a in D by A6, XBOOLE_0:def_5; then consider G being Subset of X such that A7: G is open and A8: D /\ G = {a} by A3, Th26; A9: now__::_thesis:_not_A_/\_G_=_{a} assume A /\ G = {a} ; ::_thesis: contradiction then {a} c= A by XBOOLE_1:17; then a in A by ZFMISC_1:31; hence contradiction by A6, XBOOLE_0:def_5; ::_thesis: verum end; A /\ G c= D /\ G by A4, XBOOLE_1:26; then ( A /\ G = {} or A /\ G = {a} ) by A8, ZFMISC_1:33; then ( A misses G or A /\ G = {a} ) by XBOOLE_0:def_7; then Cl A misses G by A7, A9, TSEP_1:36; then A10: (Cl A) /\ G = {} by XBOOLE_0:def_7; now__::_thesis:_not_Cl_A_=_the_carrier_of_X assume Cl A = the carrier of X ; ::_thesis: contradiction then G = {} by A10, XBOOLE_1:28; hence contradiction by A8; ::_thesis: verum end; hence contradiction by A1, TOPS_3:def_2; ::_thesis: verum end; theorem Th43: :: TEX_2:43 for X being non empty discrete TopSpace for A being Subset of X holds ( A is maximal_discrete iff not A is proper ) proof let X be non empty discrete TopSpace; ::_thesis: for A being Subset of X holds ( A is maximal_discrete iff not A is proper ) let A be Subset of X; ::_thesis: ( A is maximal_discrete iff not A is proper ) hereby ::_thesis: ( not A is proper implies A is maximal_discrete ) X is SubSpace of X by TSEP_1:2; then reconsider C = the carrier of X as Subset of X by TSEP_1:1; assume A1: A is maximal_discrete ; ::_thesis: not A is proper C is discrete by Th21; then A = C by A1, Def5; hence not A is proper by SUBSET_1:def_6; ::_thesis: verum end; hereby ::_thesis: verum assume not A is proper ; ::_thesis: A is maximal_discrete then A2: A = the carrier of X by SUBSET_1:def_6; then A3: for D being Subset of X st D is discrete & A c= D holds A = D by XBOOLE_0:def_10; A is discrete by A2, Th21; hence A is maximal_discrete by A3, Def5; ::_thesis: verum end; end; theorem Th44: :: TEX_2:44 for X being non empty anti-discrete TopSpace for A being non empty Subset of X holds ( A is maximal_discrete iff A is trivial ) proof let X be non empty anti-discrete TopSpace; ::_thesis: for A being non empty Subset of X holds ( A is maximal_discrete iff A is trivial ) let A be non empty Subset of X; ::_thesis: ( A is maximal_discrete iff A is trivial ) hereby ::_thesis: ( A is trivial implies A is maximal_discrete ) assume A is maximal_discrete ; ::_thesis: A is trivial then A is discrete by Def5; hence A is trivial by Th38; ::_thesis: verum end; hereby ::_thesis: verum A1: now__::_thesis:_for_D_being_Subset_of_X_st_D_is_discrete_&_A_c=_D_holds_ A_=_D let D be Subset of X; ::_thesis: ( D is discrete & A c= D implies A = D ) assume A2: D is discrete ; ::_thesis: ( A c= D implies A = D ) assume A3: A c= D ; ::_thesis: A = D then reconsider E = D as non empty Subset of X ; E is trivial by A2, Th38; hence A = D by A3, Th1; ::_thesis: verum end; assume A is trivial ; ::_thesis: A is maximal_discrete then A is discrete by Th38; hence A is maximal_discrete by A1, Def5; ::_thesis: verum end; end; definition let Y be non empty TopStruct ; let IT be SubSpace of Y; attrIT is maximal_discrete means :Def6: :: TEX_2:def 6 for A being Subset of Y st A = the carrier of IT holds A is maximal_discrete ; end; :: deftheorem Def6 defines maximal_discrete TEX_2:def_6_:_ for Y being non empty TopStruct for IT being SubSpace of Y holds ( IT is maximal_discrete iff for A being Subset of Y st A = the carrier of IT holds A is maximal_discrete ); theorem Th45: :: TEX_2:45 for Y being non empty TopStruct for Y0 being SubSpace of Y for A being Subset of Y st A = the carrier of Y0 holds ( A is maximal_discrete iff Y0 is maximal_discrete ) proof let Y be non empty TopStruct ; ::_thesis: for Y0 being SubSpace of Y for A being Subset of Y st A = the carrier of Y0 holds ( A is maximal_discrete iff Y0 is maximal_discrete ) let Y0 be SubSpace of Y; ::_thesis: for A being Subset of Y st A = the carrier of Y0 holds ( A is maximal_discrete iff Y0 is maximal_discrete ) let A be Subset of Y; ::_thesis: ( A = the carrier of Y0 implies ( A is maximal_discrete iff Y0 is maximal_discrete ) ) assume A1: A = the carrier of Y0 ; ::_thesis: ( A is maximal_discrete iff Y0 is maximal_discrete ) hereby ::_thesis: ( Y0 is maximal_discrete implies A is maximal_discrete ) assume A is maximal_discrete ; ::_thesis: Y0 is maximal_discrete then for A being Subset of Y st A = the carrier of Y0 holds A is maximal_discrete by A1; hence Y0 is maximal_discrete by Def6; ::_thesis: verum end; thus ( Y0 is maximal_discrete implies A is maximal_discrete ) by A1, Def6; ::_thesis: verum end; registration let Y be non empty TopStruct ; cluster non empty maximal_discrete -> non empty discrete for SubSpace of Y; coherence for b1 being non empty SubSpace of Y st b1 is maximal_discrete holds b1 is discrete proof let Y0 be non empty SubSpace of Y; ::_thesis: ( Y0 is maximal_discrete implies Y0 is discrete ) reconsider A = the carrier of Y0 as Subset of Y by Lm1; assume Y0 is maximal_discrete ; ::_thesis: Y0 is discrete then A is maximal_discrete by Def6; then A is discrete by Def5; hence Y0 is discrete by Th20; ::_thesis: verum end; cluster non empty non discrete -> non empty non maximal_discrete for SubSpace of Y; coherence for b1 being non empty SubSpace of Y st not b1 is discrete holds not b1 is maximal_discrete ; end; theorem :: TEX_2:46 for X being non empty TopSpace for X0 being non empty SubSpace of X holds ( X0 is maximal_discrete iff ( X0 is discrete & ( for Y0 being non empty discrete SubSpace of X st X0 is SubSpace of Y0 holds TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) ) ) proof let X be non empty TopSpace; ::_thesis: for X0 being non empty SubSpace of X holds ( X0 is maximal_discrete iff ( X0 is discrete & ( for Y0 being non empty discrete SubSpace of X st X0 is SubSpace of Y0 holds TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) ) ) let X0 be non empty SubSpace of X; ::_thesis: ( X0 is maximal_discrete iff ( X0 is discrete & ( for Y0 being non empty discrete SubSpace of X st X0 is SubSpace of Y0 holds TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) ) ) reconsider A = the carrier of X0 as Subset of X by TSEP_1:1; hereby ::_thesis: ( X0 is discrete & ( for Y0 being non empty discrete SubSpace of X st X0 is SubSpace of Y0 holds TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) implies X0 is maximal_discrete ) assume X0 is maximal_discrete ; ::_thesis: ( X0 is discrete & ( for Y0 being non empty discrete SubSpace of X st X0 is SubSpace of Y0 holds TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) ) then A1: A is maximal_discrete by Th45; then A is discrete by Def5; hence X0 is discrete by Th20; ::_thesis: for Y0 being non empty discrete SubSpace of X st X0 is SubSpace of Y0 holds TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) thus for Y0 being non empty discrete SubSpace of X st X0 is SubSpace of Y0 holds TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ::_thesis: verum proof let Y0 be non empty discrete SubSpace of X; ::_thesis: ( X0 is SubSpace of Y0 implies TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) reconsider D = the carrier of Y0 as Subset of X by TSEP_1:1; assume X0 is SubSpace of Y0 ; ::_thesis: TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) then A2: A c= D by TSEP_1:4; D is discrete by Th20; then A = D by A1, A2, Def5; hence TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) by TSEP_1:5; ::_thesis: verum end; end; hereby ::_thesis: verum assume X0 is discrete ; ::_thesis: ( ( for Y0 being non empty discrete SubSpace of X st X0 is SubSpace of Y0 holds TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) implies X0 is maximal_discrete ) then A3: A is discrete by Th20; assume A4: for Y0 being non empty discrete SubSpace of X st X0 is SubSpace of Y0 holds TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ; ::_thesis: X0 is maximal_discrete now__::_thesis:_for_D_being_Subset_of_X_st_D_is_discrete_&_A_c=_D_holds_ A_=_D let D be Subset of X; ::_thesis: ( D is discrete & A c= D implies A = D ) assume A5: D is discrete ; ::_thesis: ( A c= D implies A = D ) assume A6: A c= D ; ::_thesis: A = D then D <> {} ; then consider Y0 being non empty strict discrete SubSpace of X such that A7: D = the carrier of Y0 by A5, Th28; X0 is SubSpace of Y0 by A6, A7, TSEP_1:4; hence A = D by A4, A7; ::_thesis: verum end; then A is maximal_discrete by A3, Def5; hence X0 is maximal_discrete by Th45; ::_thesis: verum end; end; theorem Th47: :: TEX_2:47 for X being non empty TopSpace for A0 being non empty Subset of X st A0 is maximal_discrete holds ex X0 being non empty strict SubSpace of X st ( X0 is maximal_discrete & A0 = the carrier of X0 ) proof let X be non empty TopSpace; ::_thesis: for A0 being non empty Subset of X st A0 is maximal_discrete holds ex X0 being non empty strict SubSpace of X st ( X0 is maximal_discrete & A0 = the carrier of X0 ) let A0 be non empty Subset of X; ::_thesis: ( A0 is maximal_discrete implies ex X0 being non empty strict SubSpace of X st ( X0 is maximal_discrete & A0 = the carrier of X0 ) ) assume A1: A0 is maximal_discrete ; ::_thesis: ex X0 being non empty strict SubSpace of X st ( X0 is maximal_discrete & A0 = the carrier of X0 ) consider X0 being non empty strict SubSpace of X such that A2: A0 = the carrier of X0 by TSEP_1:10; take X0 ; ::_thesis: ( X0 is maximal_discrete & A0 = the carrier of X0 ) thus ( X0 is maximal_discrete & A0 = the carrier of X0 ) by A1, A2, Th45; ::_thesis: verum end; registration let X be non empty discrete TopSpace; cluster maximal_discrete -> non proper for SubSpace of X; coherence for b1 being SubSpace of X st b1 is maximal_discrete holds not b1 is proper proof let Y0 be SubSpace of X; ::_thesis: ( Y0 is maximal_discrete implies not Y0 is proper ) reconsider A = the carrier of Y0 as Subset of X by Lm1; assume Y0 is maximal_discrete ; ::_thesis: not Y0 is proper then A1: A is maximal_discrete by Def6; now__::_thesis:_ex_A_being_Subset_of_X_st_ (_A_=_the_carrier_of_Y0_&_not_A_is_proper_) take A = A; ::_thesis: ( A = the carrier of Y0 & not A is proper ) thus A = the carrier of Y0 ; ::_thesis: not A is proper thus not A is proper by A1, Th43; ::_thesis: verum end; hence not Y0 is proper by Def1; ::_thesis: verum end; cluster proper -> non maximal_discrete for SubSpace of X; coherence for b1 being SubSpace of X st b1 is proper holds not b1 is maximal_discrete ; cluster non proper -> maximal_discrete for SubSpace of X; coherence for b1 being SubSpace of X st not b1 is proper holds b1 is maximal_discrete proof let Y0 be SubSpace of X; ::_thesis: ( not Y0 is proper implies Y0 is maximal_discrete ) reconsider A = the carrier of Y0 as Subset of X by Lm1; assume not Y0 is proper ; ::_thesis: Y0 is maximal_discrete then not A is proper by Th8; then for A being Subset of X st A = the carrier of Y0 holds A is maximal_discrete by Th43; hence Y0 is maximal_discrete by Def6; ::_thesis: verum end; cluster non maximal_discrete -> proper for SubSpace of X; coherence for b1 being SubSpace of X st not b1 is maximal_discrete holds b1 is proper ; end; registration let X be non empty anti-discrete TopSpace; cluster non empty maximal_discrete -> non empty trivial for SubSpace of X; coherence for b1 being non empty SubSpace of X st b1 is maximal_discrete holds b1 is trivial ; cluster non empty non trivial -> non empty non maximal_discrete for SubSpace of X; coherence for b1 being non empty SubSpace of X st not b1 is trivial holds not b1 is maximal_discrete ; cluster non empty trivial -> non empty maximal_discrete for SubSpace of X; coherence for b1 being non empty SubSpace of X st b1 is trivial holds b1 is maximal_discrete proof let Y0 be non empty SubSpace of X; ::_thesis: ( Y0 is trivial implies Y0 is maximal_discrete ) assume Y0 is trivial ; ::_thesis: Y0 is maximal_discrete then for A being Subset of X st A = the carrier of Y0 holds A is maximal_discrete by Th44; hence Y0 is maximal_discrete by Def6; ::_thesis: verum end; cluster non empty non maximal_discrete -> non empty non trivial for SubSpace of X; coherence for b1 being non empty SubSpace of X st not b1 is maximal_discrete holds not b1 is trivial ; end; begin scheme :: TEX_2:sch 1 ExChoiceFCol{ F1() -> non empty TopStruct , F2() -> Subset-Family of F1(), P1[ set , set ] } : ex f being Function of F2(), the carrier of F1() st for S being Subset of F1() st S in F2() holds P1[S,f . S] provided A1: for S being Subset of F1() st S in F2() holds ex x being Point of F1() st P1[S,x] proof defpred S1[ set , set ] means ( $2 in the carrier of F1() & P1[$1,$2] ); A2: for S being set st S in F2() holds ex x being set st ( x in the carrier of F1() & S1[S,x] ) proof let S be set ; ::_thesis: ( S in F2() implies ex x being set st ( x in the carrier of F1() & S1[S,x] ) ) assume A3: S in F2() ; ::_thesis: ex x being set st ( x in the carrier of F1() & S1[S,x] ) then reconsider Q = S as Subset of F1() ; consider x being Point of F1() such that A4: P1[Q,x] by A1, A3; take x ; ::_thesis: ( x in the carrier of F1() & S1[S,x] ) thus ( x in the carrier of F1() & S1[S,x] ) by A4; ::_thesis: verum end; consider f being Function such that A5: dom f = F2() and A6: rng f c= the carrier of F1() and A7: for S being set st S in F2() holds S1[S,f . S] from FUNCT_1:sch_5(A2); reconsider f = f as Function of F2(), the carrier of F1() by A5, A6, FUNCT_2:def_1, RELSET_1:4; take f ; ::_thesis: for S being Subset of F1() st S in F2() holds P1[S,f . S] thus for S being Subset of F1() st S in F2() holds P1[S,f . S] by A7; ::_thesis: verum end; theorem Th48: :: TEX_2:48 for X being non empty almost_discrete TopSpace for A being Subset of X holds Cl A = union { (Cl {a}) where a is Point of X : a in A } proof let X be non empty almost_discrete TopSpace; ::_thesis: for A being Subset of X holds Cl A = union { (Cl {a}) where a is Point of X : a in A } let A be Subset of X; ::_thesis: Cl A = union { (Cl {a}) where a is Point of X : a in A } set F = { (Cl {a}) where a is Point of X : a in A } ; now__::_thesis:_for_C_being_set_st_C_in__{__(Cl_{a})_where_a_is_Point_of_X_:_a_in_A__}__holds_ C_in_bool_the_carrier_of_X let C be set ; ::_thesis: ( C in { (Cl {a}) where a is Point of X : a in A } implies C in bool the carrier of X ) assume C in { (Cl {a}) where a is Point of X : a in A } ; ::_thesis: C in bool the carrier of X then ex a being Point of X st ( C = Cl {a} & a in A ) ; hence C in bool the carrier of X ; ::_thesis: verum end; then reconsider F = { (Cl {a}) where a is Point of X : a in A } as Subset-Family of X by TARSKI:def_3; reconsider F = F as Subset-Family of X ; now__::_thesis:_for_x_being_set_st_x_in_A_holds_ x_in_union_F let x be set ; ::_thesis: ( x in A implies x in union F ) assume A1: x in A ; ::_thesis: x in union F then reconsider a = x as Point of X ; Cl {a} in F by A1; then A2: Cl {a} c= union F by ZFMISC_1:74; A3: {a} c= Cl {a} by PRE_TOPC:18; a in {a} by TARSKI:def_1; then a in Cl {a} by A3; hence x in union F by A2; ::_thesis: verum end; then A4: A c= union F by TARSKI:def_3; now__::_thesis:_for_C_being_set_st_C_in_F_holds_ C_c=_Cl_A let C be set ; ::_thesis: ( C in F implies C c= Cl A ) assume C in F ; ::_thesis: C c= Cl A then consider a being Point of X such that A5: C = Cl {a} and A6: a in A ; {a} c= A by A6, ZFMISC_1:31; hence C c= Cl A by A5, PRE_TOPC:19; ::_thesis: verum end; then A7: union F c= Cl A by ZFMISC_1:76; now__::_thesis:_for_G_being_Subset_of_X_st_G_in_F_holds_ G_is_open let G be Subset of X; ::_thesis: ( G in F implies G is open ) assume G in F ; ::_thesis: G is open then ex a being Point of X st ( G = Cl {a} & a in A ) ; hence G is open by TDLAT_3:22; ::_thesis: verum end; then F is open by TOPS_2:def_1; then union F is open by TOPS_2:19; then union F is closed by TDLAT_3:21; then Cl A c= union F by A4, TOPS_1:5; hence Cl A = union { (Cl {a}) where a is Point of X : a in A } by A7, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th49: :: TEX_2:49 for X being non empty almost_discrete TopSpace for a, b being Point of X st a in Cl {b} holds Cl {a} = Cl {b} proof let X be non empty almost_discrete TopSpace; ::_thesis: for a, b being Point of X st a in Cl {b} holds Cl {a} = Cl {b} let a, b be Point of X; ::_thesis: ( a in Cl {b} implies Cl {a} = Cl {b} ) assume a in Cl {b} ; ::_thesis: Cl {a} = Cl {b} then A1: {a} c= Cl {b} by ZFMISC_1:31; b in Cl {a} proof assume not b in Cl {a} ; ::_thesis: contradiction then A2: {b} misses Cl {a} by ZFMISC_1:50; Cl {a} is open by TDLAT_3:22; then Cl {b} misses Cl {a} by A2, TSEP_1:36; then (Cl {b}) /\ (Cl {a}) = {} by XBOOLE_0:def_7; then Cl {a} = {} by A1, TOPS_1:5, XBOOLE_1:28; hence contradiction by PRE_TOPC:18, XBOOLE_1:3; ::_thesis: verum end; then {b} c= Cl {a} by ZFMISC_1:31; then A3: Cl {b} c= Cl {a} by TOPS_1:5; Cl {a} c= Cl {b} by A1, TOPS_1:5; hence Cl {a} = Cl {b} by A3, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th50: :: TEX_2:50 for X being non empty almost_discrete TopSpace for a, b being Point of X holds ( Cl {a} misses Cl {b} or Cl {a} = Cl {b} ) proof let X be non empty almost_discrete TopSpace; ::_thesis: for a, b being Point of X holds ( Cl {a} misses Cl {b} or Cl {a} = Cl {b} ) let a, b be Point of X; ::_thesis: ( Cl {a} misses Cl {b} or Cl {a} = Cl {b} ) assume (Cl {a}) /\ (Cl {b}) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: Cl {a} = Cl {b} then consider x being set such that A1: x in (Cl {a}) /\ (Cl {b}) by XBOOLE_0:def_1; reconsider x = x as Point of X by A1; x in Cl {a} by A1, XBOOLE_0:def_4; then A2: Cl {x} = Cl {a} by Th49; x in Cl {b} by A1, XBOOLE_0:def_4; hence Cl {a} = Cl {b} by A2, Th49; ::_thesis: verum end; theorem Th51: :: TEX_2:51 for X being non empty almost_discrete TopSpace for A being Subset of X st ( for x being Point of X st x in A holds ex F being Subset of X st ( F is closed & A /\ F = {x} ) ) holds A is discrete proof let X be non empty almost_discrete TopSpace; ::_thesis: for A being Subset of X st ( for x being Point of X st x in A holds ex F being Subset of X st ( F is closed & A /\ F = {x} ) ) holds A is discrete let A be Subset of X; ::_thesis: ( ( for x being Point of X st x in A holds ex F being Subset of X st ( F is closed & A /\ F = {x} ) ) implies A is discrete ) assume A1: for x being Point of X st x in A holds ex F being Subset of X st ( F is closed & A /\ F = {x} ) ; ::_thesis: A is discrete now__::_thesis:_for_x_being_Point_of_X_st_x_in_A_holds_ ex_G_being_Subset_of_X_st_ (_G_is_open_&_A_/\_G_=_{x}_) let x be Point of X; ::_thesis: ( x in A implies ex G being Subset of X st ( G is open & A /\ G = {x} ) ) assume A2: x in A ; ::_thesis: ex G being Subset of X st ( G is open & A /\ G = {x} ) now__::_thesis:_ex_F_being_Subset_of_X_st_ (_F_is_open_&_A_/\_F_=_{x}_) consider F being Subset of X such that A3: F is closed and A4: A /\ F = {x} by A1, A2; take F = F; ::_thesis: ( F is open & A /\ F = {x} ) thus F is open by A3, TDLAT_3:22; ::_thesis: A /\ F = {x} thus A /\ F = {x} by A4; ::_thesis: verum end; hence ex G being Subset of X st ( G is open & A /\ G = {x} ) ; ::_thesis: verum end; hence A is discrete by Th31; ::_thesis: verum end; theorem Th52: :: TEX_2:52 for X being non empty almost_discrete TopSpace for A being Subset of X st ( for x being Point of X st x in A holds A /\ (Cl {x}) = {x} ) holds A is discrete proof let X be non empty almost_discrete TopSpace; ::_thesis: for A being Subset of X st ( for x being Point of X st x in A holds A /\ (Cl {x}) = {x} ) holds A is discrete let A be Subset of X; ::_thesis: ( ( for x being Point of X st x in A holds A /\ (Cl {x}) = {x} ) implies A is discrete ) assume A1: for x being Point of X st x in A holds A /\ (Cl {x}) = {x} ; ::_thesis: A is discrete now__::_thesis:_for_x_being_Point_of_X_st_x_in_A_holds_ ex_F_being_Subset_of_X_st_ (_F_is_closed_&_A_/\_F_=_{x}_) let x be Point of X; ::_thesis: ( x in A implies ex F being Subset of X st ( F is closed & A /\ F = {x} ) ) assume A2: x in A ; ::_thesis: ex F being Subset of X st ( F is closed & A /\ F = {x} ) now__::_thesis:_ex_F_being_Element_of_bool_the_carrier_of_X_st_ (_F_is_closed_&_A_/\_F_=_{x}_) take F = Cl {x}; ::_thesis: ( F is closed & A /\ F = {x} ) thus F is closed ; ::_thesis: A /\ F = {x} thus A /\ F = {x} by A1, A2; ::_thesis: verum end; hence ex F being Subset of X st ( F is closed & A /\ F = {x} ) ; ::_thesis: verum end; hence A is discrete by Th51; ::_thesis: verum end; theorem :: TEX_2:53 for X being non empty almost_discrete TopSpace for A being Subset of X holds ( A is discrete iff for a, b being Point of X st a in A & b in A & a <> b holds Cl {a} misses Cl {b} ) proof let X be non empty almost_discrete TopSpace; ::_thesis: for A being Subset of X holds ( A is discrete iff for a, b being Point of X st a in A & b in A & a <> b holds Cl {a} misses Cl {b} ) let A be Subset of X; ::_thesis: ( A is discrete iff for a, b being Point of X st a in A & b in A & a <> b holds Cl {a} misses Cl {b} ) thus ( A is discrete implies for a, b being Point of X st a in A & b in A & a <> b holds Cl {a} misses Cl {b} ) ::_thesis: ( ( for a, b being Point of X st a in A & b in A & a <> b holds Cl {a} misses Cl {b} ) implies A is discrete ) proof assume A1: A is discrete ; ::_thesis: for a, b being Point of X st a in A & b in A & a <> b holds Cl {a} misses Cl {b} let a, b be Point of X; ::_thesis: ( a in A & b in A & a <> b implies Cl {a} misses Cl {b} ) assume that A2: a in A and A3: b in A ; ::_thesis: ( not a <> b or Cl {a} misses Cl {b} ) A4: A /\ (Cl {b}) = {b} by A1, A3, Th36; assume A5: a <> b ; ::_thesis: Cl {a} misses Cl {b} assume (Cl {a}) /\ (Cl {b}) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction then A6: Cl {a} meets Cl {b} by XBOOLE_0:def_7; A /\ (Cl {a}) = {a} by A1, A2, Th36; then {a} = {b} by A4, A6, Th50; hence contradiction by A5, ZFMISC_1:3; ::_thesis: verum end; assume A7: for a, b being Point of X st a in A & b in A & a <> b holds Cl {a} misses Cl {b} ; ::_thesis: A is discrete now__::_thesis:_for_x_being_Point_of_X_st_x_in_A_holds_ not_A_/\_(Cl_{x})_<>_{x} let x be Point of X; ::_thesis: ( x in A implies not A /\ (Cl {x}) <> {x} ) assume A8: x in A ; ::_thesis: not A /\ (Cl {x}) <> {x} assume A9: A /\ (Cl {x}) <> {x} ; ::_thesis: contradiction A10: {x} c= Cl {x} by PRE_TOPC:18; {x} c= A by A8, ZFMISC_1:31; then (A /\ (Cl {x})) \ {x} <> {} by A10, A9, Lm3, XBOOLE_1:19; then consider y being set such that A11: y in (A /\ (Cl {x})) \ {x} by XBOOLE_0:def_1; reconsider y = y as Point of X by A11; not y in {x} by A11, XBOOLE_0:def_5; then A12: y <> x by TARSKI:def_1; A13: y in A /\ (Cl {x}) by A11, XBOOLE_0:def_5; then y in A by XBOOLE_0:def_4; then Cl {y} misses Cl {x} by A7, A8, A12; then A14: (Cl {y}) /\ (Cl {x}) = {} by XBOOLE_0:def_7; y in Cl {x} by A13, XBOOLE_0:def_4; then Cl {y} = Cl {x} by Th49; hence contradiction by A14, PRE_TOPC:18, XBOOLE_1:3; ::_thesis: verum end; hence A is discrete by Th52; ::_thesis: verum end; theorem Th54: :: TEX_2:54 for X being non empty almost_discrete TopSpace for A being Subset of X holds ( A is discrete iff for x being Point of X st x in Cl A holds ex a being Point of X st ( a in A & A /\ (Cl {x}) = {a} ) ) proof let X be non empty almost_discrete TopSpace; ::_thesis: for A being Subset of X holds ( A is discrete iff for x being Point of X st x in Cl A holds ex a being Point of X st ( a in A & A /\ (Cl {x}) = {a} ) ) let A be Subset of X; ::_thesis: ( A is discrete iff for x being Point of X st x in Cl A holds ex a being Point of X st ( a in A & A /\ (Cl {x}) = {a} ) ) thus ( A is discrete implies for x being Point of X st x in Cl A holds ex a being Point of X st ( a in A & A /\ (Cl {x}) = {a} ) ) ::_thesis: ( ( for x being Point of X st x in Cl A holds ex a being Point of X st ( a in A & A /\ (Cl {x}) = {a} ) ) implies A is discrete ) proof assume A1: A is discrete ; ::_thesis: for x being Point of X st x in Cl A holds ex a being Point of X st ( a in A & A /\ (Cl {x}) = {a} ) let x be Point of X; ::_thesis: ( x in Cl A implies ex a being Point of X st ( a in A & A /\ (Cl {x}) = {a} ) ) A2: Cl A = union { (Cl {a}) where a is Point of X : a in A } by Th48; assume x in Cl A ; ::_thesis: ex a being Point of X st ( a in A & A /\ (Cl {x}) = {a} ) then consider C being set such that A3: x in C and A4: C in { (Cl {a}) where a is Point of X : a in A } by A2, TARSKI:def_4; consider a being Point of X such that A5: C = Cl {a} and A6: a in A by A4; now__::_thesis:_ex_a_being_Point_of_X_st_ (_a_in_A_&_A_/\_(Cl_{x})_=_{a}_) take a = a; ::_thesis: ( a in A & A /\ (Cl {x}) = {a} ) thus a in A by A6; ::_thesis: A /\ (Cl {x}) = {a} Cl {x} = Cl {a} by A3, A5, Th49; hence A /\ (Cl {x}) = {a} by A1, A6, Th36; ::_thesis: verum end; hence ex a being Point of X st ( a in A & A /\ (Cl {x}) = {a} ) ; ::_thesis: verum end; assume A7: for x being Point of X st x in Cl A holds ex a being Point of X st ( a in A & A /\ (Cl {x}) = {a} ) ; ::_thesis: A is discrete for x being Point of X st x in A holds A /\ (Cl {x}) = {x} proof let x be Point of X; ::_thesis: ( x in A implies A /\ (Cl {x}) = {x} ) assume A8: x in A ; ::_thesis: A /\ (Cl {x}) = {x} A c= Cl A by PRE_TOPC:18; then A9: ex a being Point of X st ( a in A & A /\ (Cl {x}) = {a} ) by A7, A8; A10: {x} c= Cl {x} by PRE_TOPC:18; {x} c= A by A8, ZFMISC_1:31; hence A /\ (Cl {x}) = {x} by A9, A10, XBOOLE_1:19, ZFMISC_1:18; ::_thesis: verum end; hence A is discrete by Th52; ::_thesis: verum end; theorem :: TEX_2:55 for X being non empty almost_discrete TopSpace for A being Subset of X st ( A is open or A is closed ) & A is maximal_discrete holds not A is proper proof let X be non empty almost_discrete TopSpace; ::_thesis: for A being Subset of X st ( A is open or A is closed ) & A is maximal_discrete holds not A is proper let A be Subset of X; ::_thesis: ( ( A is open or A is closed ) & A is maximal_discrete implies not A is proper ) assume A1: ( A is open or A is closed ) ; ::_thesis: ( not A is maximal_discrete or not A is proper ) then A is closed by TDLAT_3:21; then A2: A = Cl A by PRE_TOPC:22; assume A3: A is maximal_discrete ; ::_thesis: not A is proper A is open by A1, TDLAT_3:22; then A is dense by A3, Th41; then A = the carrier of X by A2, TOPS_3:def_2; hence not A is proper by SUBSET_1:def_6; ::_thesis: verum end; theorem Th56: :: TEX_2:56 for X being non empty almost_discrete TopSpace for A being Subset of X st A is maximal_discrete holds A is dense proof let X be non empty almost_discrete TopSpace; ::_thesis: for A being Subset of X st A is maximal_discrete holds A is dense let A be Subset of X; ::_thesis: ( A is maximal_discrete implies A is dense ) assume A1: A is maximal_discrete ; ::_thesis: A is dense then A2: A is discrete by Def5; assume not A is dense ; ::_thesis: contradiction then Cl A <> the carrier of X by TOPS_3:def_2; then the carrier of X \ (Cl A) <> {} by Lm3; then consider a being set such that A3: a in the carrier of X \ (Cl A) by XBOOLE_0:def_1; reconsider a = a as Point of X by A3; set B = A \/ {a}; A4: A c= A \/ {a} by XBOOLE_1:7; A5: now__::_thesis:_for_x_being_Point_of_X_st_x_in_A_\/_{a}_holds_ ex_G_being_Subset_of_X_st_ (_G_is_open_&_(A_\/_{a})_/\_G_=_{x}_) let x be Point of X; ::_thesis: ( x in A \/ {a} implies ex G being Subset of X st ( G is open & (A \/ {a}) /\ G = {x} ) ) assume x in A \/ {a} ; ::_thesis: ex G being Subset of X st ( G is open & (A \/ {a}) /\ G = {x} ) then A6: ( x in A or x in {a} ) by XBOOLE_0:def_3; now__::_thesis:_ex_E_being_Subset_of_X_st_ (_E_is_open_&_(A_\/_{a})_/\_E_=_{x}_) percases ( x in A or x = a ) by A6, TARSKI:def_1; supposeA7: x in A ; ::_thesis: ex E being Subset of X st ( E is open & (A \/ {a}) /\ E = {x} ) then consider G being Subset of X such that A8: G is open and A9: A /\ G = {x} by A2, Th26; now__::_thesis:_ex_E_being_Element_of_bool_the_carrier_of_X_st_ (_E_is_open_&_(A_\/_{a})_/\_E_=_{x}_) take E = (Cl A) /\ G; ::_thesis: ( E is open & (A \/ {a}) /\ E = {x} ) A10: (A \/ {a}) /\ E = (A /\ E) \/ ({a} /\ E) by XBOOLE_1:23; Cl A is open by TDLAT_3:22; hence E is open by A8; ::_thesis: (A \/ {a}) /\ E = {x} A11: {x} c= E by A9, PRE_TOPC:18, XBOOLE_1:26; E c= Cl A by XBOOLE_1:17; then not a in E by A3, XBOOLE_0:def_5; then {a} misses E by ZFMISC_1:50; then A12: {a} /\ E = {} by XBOOLE_0:def_7; {x} c= A \/ {a} by A4, A7, ZFMISC_1:31; then A13: {x} c= (A \/ {a}) /\ E by A11, XBOOLE_1:19; A /\ E c= A /\ G by XBOOLE_1:17, XBOOLE_1:26; hence (A \/ {a}) /\ E = {x} by A9, A13, A12, A10, XBOOLE_0:def_10; ::_thesis: verum end; hence ex E being Subset of X st ( E is open & (A \/ {a}) /\ E = {x} ) ; ::_thesis: verum end; supposeA14: x = a ; ::_thesis: ex G being Subset of X st ( G is open & (A \/ {a}) /\ G = {x} ) now__::_thesis:_ex_G_being_Element_of_bool_the_carrier_of_X_st_ (_G_is_open_&_(A_\/_{a})_/\_G_=_{x}_) take G = ([#] X) \ (Cl A); ::_thesis: ( G is open & (A \/ {a}) /\ G = {x} ) A15: (A \/ {a}) /\ G = (A /\ G) \/ ({a} /\ G) by XBOOLE_1:23; A16: G = (Cl A) ` ; hence G is open ; ::_thesis: (A \/ {a}) /\ G = {x} A c= Cl A by PRE_TOPC:18; then A misses G by A16, SUBSET_1:24; then A17: A /\ G = {} by XBOOLE_0:def_7; {a} c= G by A3, ZFMISC_1:31; hence (A \/ {a}) /\ G = {x} by A14, A17, A15, XBOOLE_1:28; ::_thesis: verum end; hence ex G being Subset of X st ( G is open & (A \/ {a}) /\ G = {x} ) ; ::_thesis: verum end; end; end; hence ex G being Subset of X st ( G is open & (A \/ {a}) /\ G = {x} ) ; ::_thesis: verum end; A c= Cl A by PRE_TOPC:18; then A18: not a in A by A3, XBOOLE_0:def_5; ex D being Subset of X st ( D is discrete & A c= D & A <> D ) proof take A \/ {a} ; ::_thesis: ( A \/ {a} is discrete & A c= A \/ {a} & A <> A \/ {a} ) thus A \/ {a} is discrete by A5, Th31; ::_thesis: ( A c= A \/ {a} & A <> A \/ {a} ) thus A c= A \/ {a} by XBOOLE_1:7; ::_thesis: A <> A \/ {a} now__::_thesis:_not_A_=_A_\/_{a} assume A = A \/ {a} ; ::_thesis: contradiction then {a} c= A by XBOOLE_1:7; hence contradiction by A18, ZFMISC_1:31; ::_thesis: verum end; hence A <> A \/ {a} ; ::_thesis: verum end; hence contradiction by A1, Def5; ::_thesis: verum end; theorem Th57: :: TEX_2:57 for X being non empty almost_discrete TopSpace for A being Subset of X st A is maximal_discrete holds union { (Cl {a}) where a is Point of X : a in A } = the carrier of X proof let X be non empty almost_discrete TopSpace; ::_thesis: for A being Subset of X st A is maximal_discrete holds union { (Cl {a}) where a is Point of X : a in A } = the carrier of X let A be Subset of X; ::_thesis: ( A is maximal_discrete implies union { (Cl {a}) where a is Point of X : a in A } = the carrier of X ) assume A is maximal_discrete ; ::_thesis: union { (Cl {a}) where a is Point of X : a in A } = the carrier of X then A is dense by Th56; then Cl A = the carrier of X by TOPS_3:def_2; hence union { (Cl {a}) where a is Point of X : a in A } = the carrier of X by Th48; ::_thesis: verum end; theorem Th58: :: TEX_2:58 for X being non empty almost_discrete TopSpace for A being Subset of X holds ( A is maximal_discrete iff for x being Point of X ex a being Point of X st ( a in A & A /\ (Cl {x}) = {a} ) ) proof let X be non empty almost_discrete TopSpace; ::_thesis: for A being Subset of X holds ( A is maximal_discrete iff for x being Point of X ex a being Point of X st ( a in A & A /\ (Cl {x}) = {a} ) ) let A be Subset of X; ::_thesis: ( A is maximal_discrete iff for x being Point of X ex a being Point of X st ( a in A & A /\ (Cl {x}) = {a} ) ) thus ( A is maximal_discrete implies for x being Point of X ex a being Point of X st ( a in A & A /\ (Cl {x}) = {a} ) ) ::_thesis: ( ( for x being Point of X ex a being Point of X st ( a in A & A /\ (Cl {x}) = {a} ) ) implies A is maximal_discrete ) proof assume A1: A is maximal_discrete ; ::_thesis: for x being Point of X ex a being Point of X st ( a in A & A /\ (Cl {x}) = {a} ) let x be Point of X; ::_thesis: ex a being Point of X st ( a in A & A /\ (Cl {x}) = {a} ) the carrier of X = union { (Cl {a}) where a is Point of X : a in A } by A1, Th57; then consider C being set such that A2: x in C and A3: C in { (Cl {a}) where a is Point of X : a in A } by TARSKI:def_4; consider a being Point of X such that A4: C = Cl {a} and A5: a in A by A3; A6: A is discrete by A1, Def5; now__::_thesis:_ex_a_being_Point_of_X_st_ (_a_in_A_&_A_/\_(Cl_{x})_=_{a}_) take a = a; ::_thesis: ( a in A & A /\ (Cl {x}) = {a} ) thus a in A by A5; ::_thesis: A /\ (Cl {x}) = {a} Cl {x} = Cl {a} by A2, A4, Th49; hence A /\ (Cl {x}) = {a} by A6, A5, Th36; ::_thesis: verum end; hence ex a being Point of X st ( a in A & A /\ (Cl {x}) = {a} ) ; ::_thesis: verum end; assume A7: for x being Point of X ex a being Point of X st ( a in A & A /\ (Cl {x}) = {a} ) ; ::_thesis: A is maximal_discrete A8: for D being Subset of X st D is discrete & A c= D holds A = D proof let D be Subset of X; ::_thesis: ( D is discrete & A c= D implies A = D ) assume A9: D is discrete ; ::_thesis: ( not A c= D or A = D ) assume A10: A c= D ; ::_thesis: A = D now__::_thesis:_for_x_being_set_st_x_in_D_holds_ x_in_A let x be set ; ::_thesis: ( x in D implies x in A ) assume A11: x in D ; ::_thesis: x in A then reconsider y = x as Point of X ; A12: ex a being Point of X st ( a in A & A /\ (Cl {y}) = {a} ) by A7; D /\ (Cl {y}) = {y} by A9, A11, Th36; hence x in A by A10, A12, XBOOLE_1:26, ZFMISC_1:18; ::_thesis: verum end; then D c= A by TARSKI:def_3; hence A = D by A10, XBOOLE_0:def_10; ::_thesis: verum end; for x being Point of X st x in A holds A /\ (Cl {x}) = {x} proof let x be Point of X; ::_thesis: ( x in A implies A /\ (Cl {x}) = {x} ) A13: {x} c= Cl {x} by PRE_TOPC:18; assume x in A ; ::_thesis: A /\ (Cl {x}) = {x} then A14: {x} c= A by ZFMISC_1:31; ex a being Point of X st ( a in A & A /\ (Cl {x}) = {a} ) by A7; hence A /\ (Cl {x}) = {x} by A14, A13, XBOOLE_1:19, ZFMISC_1:18; ::_thesis: verum end; then A is discrete by Th52; hence A is maximal_discrete by A8, Def5; ::_thesis: verum end; theorem Th59: :: TEX_2:59 for X being non empty almost_discrete TopSpace for A being Subset of X st A is discrete holds ex M being Subset of X st ( A c= M & M is maximal_discrete ) proof let X be non empty almost_discrete TopSpace; ::_thesis: for A being Subset of X st A is discrete holds ex M being Subset of X st ( A c= M & M is maximal_discrete ) let A be Subset of X; ::_thesis: ( A is discrete implies ex M being Subset of X st ( A c= M & M is maximal_discrete ) ) set D = ([#] X) \ (Cl A); set F = { (Cl {d}) where d is Point of X : d in ([#] X) \ (Cl A) } ; now__::_thesis:_for_C_being_set_st_C_in__{__(Cl_{d})_where_d_is_Point_of_X_:_d_in_([#]_X)_\_(Cl_A)__}__holds_ C_in_bool_the_carrier_of_X let C be set ; ::_thesis: ( C in { (Cl {d}) where d is Point of X : d in ([#] X) \ (Cl A) } implies C in bool the carrier of X ) assume C in { (Cl {d}) where d is Point of X : d in ([#] X) \ (Cl A) } ; ::_thesis: C in bool the carrier of X then ex a being Point of X st ( C = Cl {a} & a in ([#] X) \ (Cl A) ) ; hence C in bool the carrier of X ; ::_thesis: verum end; then reconsider F = { (Cl {d}) where d is Point of X : d in ([#] X) \ (Cl A) } as Subset-Family of X by TARSKI:def_3; assume A1: A is discrete ; ::_thesis: ex M being Subset of X st ( A c= M & M is maximal_discrete ) defpred S1[ set , set ] means ( $2 in ([#] X) \ (Cl A) & $2 in $1 ); A2: ([#] X) \ (Cl A) = (Cl A) ` ; then ([#] X) \ (Cl A) is closed by TDLAT_3:21; then A3: ([#] X) \ (Cl A) = Cl (([#] X) \ (Cl A)) by PRE_TOPC:22; A c= Cl A by PRE_TOPC:18; then A misses ([#] X) \ (Cl A) by A2, SUBSET_1:24; then A4: A /\ (([#] X) \ (Cl A)) = {} by XBOOLE_0:def_7; reconsider F = F as Subset-Family of X ; A5: for S being Subset of X st S in F holds ex x being Point of X st S1[S,x] proof let S be Subset of X; ::_thesis: ( S in F implies ex x being Point of X st S1[S,x] ) assume S in F ; ::_thesis: ex x being Point of X st S1[S,x] then consider d being Point of X such that A6: S = Cl {d} and A7: d in ([#] X) \ (Cl A) ; take d ; ::_thesis: S1[S,d] {d} c= Cl {d} by PRE_TOPC:18; hence S1[S,d] by A6, A7, ZFMISC_1:31; ::_thesis: verum end; consider f being Function of F, the carrier of X such that A8: for S being Subset of X st S in F holds S1[S,f . S] from TEX_2:sch_1(A5); set M = A \/ (f .: F); now__::_thesis:_for_x_being_set_st_x_in_f_.:_F_holds_ x_in_([#]_X)_\_(Cl_A) let x be set ; ::_thesis: ( x in f .: F implies x in ([#] X) \ (Cl A) ) assume x in f .: F ; ::_thesis: x in ([#] X) \ (Cl A) then ex S being set st ( S in F & S in F & x = f . S ) by FUNCT_2:64; hence x in ([#] X) \ (Cl A) by A8; ::_thesis: verum end; then A9: f .: F c= ([#] X) \ (Cl A) by TARSKI:def_3; ([#] X) \ (Cl A) misses Cl A by A2, SUBSET_1:24; then A10: Cl A misses f .: F by A9, XBOOLE_1:63; thus ex M being Subset of X st ( A c= M & M is maximal_discrete ) ::_thesis: verum proof take A \/ (f .: F) ; ::_thesis: ( A c= A \/ (f .: F) & A \/ (f .: F) is maximal_discrete ) thus A11: A c= A \/ (f .: F) by XBOOLE_1:7; ::_thesis: A \/ (f .: F) is maximal_discrete for x being Point of X ex a being Point of X st ( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (Cl {x}) = {a} ) proof let x be Point of X; ::_thesis: ex a being Point of X st ( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (Cl {x}) = {a} ) A12: [#] X = (Cl A) \/ (([#] X) \ (Cl A)) by XBOOLE_1:45; now__::_thesis:_ex_a_being_Point_of_X_st_ (_a_in_A_\/_(f_.:_F)_&_(A_\/_(f_.:_F))_/\_(Cl_{x})_=_{a}_) percases ( x in Cl A or x in ([#] X) \ (Cl A) ) by A12, XBOOLE_0:def_3; supposeA13: x in Cl A ; ::_thesis: ex a being Point of X st ( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (Cl {x}) = {a} ) now__::_thesis:_ex_a_being_Point_of_X_st_ (_a_in_A_\/_(f_.:_F)_&_(A_\/_(f_.:_F))_/\_(Cl_{x})_=_{a}_) consider a being Point of X such that A14: a in A and A15: A /\ (Cl {x}) = {a} by A1, A13, Th54; take a = a; ::_thesis: ( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (Cl {x}) = {a} ) thus a in A \/ (f .: F) by A11, A14; ::_thesis: (A \/ (f .: F)) /\ (Cl {x}) = {a} {x} c= Cl A by A13, ZFMISC_1:31; then f .: F misses Cl {x} by A10, TOPS_1:5, XBOOLE_1:63; then (f .: F) /\ (Cl {x}) = {} by XBOOLE_0:def_7; then (A \/ (f .: F)) /\ (Cl {x}) = (A /\ (Cl {x})) \/ {} by XBOOLE_1:23; hence (A \/ (f .: F)) /\ (Cl {x}) = {a} by A15; ::_thesis: verum end; hence ex a being Point of X st ( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (Cl {x}) = {a} ) ; ::_thesis: verum end; supposeA16: x in ([#] X) \ (Cl A) ; ::_thesis: ex a being Point of X st ( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (Cl {x}) = {a} ) then A17: Cl {x} in F ; now__::_thesis:_ex_a_being_Point_of_X_st_ (_a_in_A_\/_(f_.:_F)_&_(A_\/_(f_.:_F))_/\_(Cl_{x})_=_{a}_) reconsider a = f . (Cl {x}) as Point of X by A17, FUNCT_2:5; take a = a; ::_thesis: ( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (Cl {x}) = {a} ) A18: f .: F c= A \/ (f .: F) by XBOOLE_1:7; now__::_thesis:_for_y_being_set_st_y_in_(A_\/_(f_.:_F))_/\_(Cl_{x})_holds_ y_in_{a} let y be set ; ::_thesis: ( y in (A \/ (f .: F)) /\ (Cl {x}) implies y in {a} ) assume A19: y in (A \/ (f .: F)) /\ (Cl {x}) ; ::_thesis: y in {a} then reconsider z = y as Point of X ; A20: z in Cl {x} by A19, XBOOLE_0:def_4; A21: z in A \/ (f .: F) by A19, XBOOLE_0:def_4; {x} c= ([#] X) \ (Cl A) by A16, ZFMISC_1:31; then Cl {x} c= ([#] X) \ (Cl A) by A3, PRE_TOPC:19; then not z in A by A4, A20, XBOOLE_0:def_4; then z in f .: F by A21, XBOOLE_0:def_3; then consider C being set such that A22: C in F and C in F and A23: z = f . C by FUNCT_2:64; reconsider C = C as Subset of X by A22; consider w being Point of X such that A24: C = Cl {w} and w in ([#] X) \ (Cl A) by A22; Cl {z} = Cl {x} by A20, Th49; then f . (Cl {w}) = a by A8, A22, A23, A24, Th49; hence y in {a} by A23, A24, TARSKI:def_1; ::_thesis: verum end; then A25: (A \/ (f .: F)) /\ (Cl {x}) c= {a} by TARSKI:def_3; A26: a in f .: F by A17, FUNCT_2:35; hence a in A \/ (f .: F) by A18; ::_thesis: (A \/ (f .: F)) /\ (Cl {x}) = {a} a in Cl {x} by A8, A17; then A27: {a} c= Cl {x} by ZFMISC_1:31; {a} c= A \/ (f .: F) by A18, A26, ZFMISC_1:31; then {a} c= (A \/ (f .: F)) /\ (Cl {x}) by A27, XBOOLE_1:19; hence (A \/ (f .: F)) /\ (Cl {x}) = {a} by A25, XBOOLE_0:def_10; ::_thesis: verum end; hence ex a being Point of X st ( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (Cl {x}) = {a} ) ; ::_thesis: verum end; end; end; hence ex a being Point of X st ( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (Cl {x}) = {a} ) ; ::_thesis: verum end; hence A \/ (f .: F) is maximal_discrete by Th58; ::_thesis: verum end; end; theorem Th60: :: TEX_2:60 for X being non empty almost_discrete TopSpace ex M being Subset of X st M is maximal_discrete proof let X be non empty almost_discrete TopSpace; ::_thesis: ex M being Subset of X st M is maximal_discrete set A = {} X; {} X is discrete by Th29; then consider M being Subset of X such that {} X c= M and A1: M is maximal_discrete by Th59; take M ; ::_thesis: M is maximal_discrete thus M is maximal_discrete by A1; ::_thesis: verum end; theorem Th61: :: TEX_2:61 for X being non empty almost_discrete TopSpace for Y0 being non empty discrete SubSpace of X ex X0 being non empty strict SubSpace of X st ( Y0 is SubSpace of X0 & X0 is maximal_discrete ) proof let X be non empty almost_discrete TopSpace; ::_thesis: for Y0 being non empty discrete SubSpace of X ex X0 being non empty strict SubSpace of X st ( Y0 is SubSpace of X0 & X0 is maximal_discrete ) let Y0 be non empty discrete SubSpace of X; ::_thesis: ex X0 being non empty strict SubSpace of X st ( Y0 is SubSpace of X0 & X0 is maximal_discrete ) reconsider A = the carrier of Y0 as Subset of X by TSEP_1:1; A is discrete by Th20; then consider M being Subset of X such that A1: A c= M and A2: M is maximal_discrete by Th59; not M is empty by A2, Th40; then consider X0 being non empty strict SubSpace of X such that A3: X0 is maximal_discrete and A4: M = the carrier of X0 by A2, Th47; take X0 ; ::_thesis: ( Y0 is SubSpace of X0 & X0 is maximal_discrete ) thus ( Y0 is SubSpace of X0 & X0 is maximal_discrete ) by A1, A3, A4, TSEP_1:4; ::_thesis: verum end; registration let X be non empty non discrete almost_discrete TopSpace; cluster non empty maximal_discrete -> non empty proper for SubSpace of X; coherence for b1 being non empty SubSpace of X st b1 is maximal_discrete holds b1 is proper proof let X0 be non empty SubSpace of X; ::_thesis: ( X0 is maximal_discrete implies X0 is proper ) reconsider A = the carrier of X0 as Subset of X by Lm1; assume X0 is maximal_discrete ; ::_thesis: X0 is proper then A is maximal_discrete by Def6; then A is discrete by Def5; then A1: X0 is discrete by Th20; X0 is proper proof assume not X0 is proper ; ::_thesis: contradiction then not A is proper by Th8; then A2: A = the carrier of X by SUBSET_1:def_6; X is SubSpace of X by TSEP_1:2; then TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of X, the topology of X #) by A2, TSEP_1:5; hence contradiction by A1, Th12; ::_thesis: verum end; hence X0 is proper ; ::_thesis: verum end; cluster non empty non proper -> non empty non maximal_discrete for SubSpace of X; coherence for b1 being non empty SubSpace of X st not b1 is proper holds not b1 is maximal_discrete ; end; registration let X be non empty non anti-discrete almost_discrete TopSpace; cluster non empty maximal_discrete -> non empty non trivial for SubSpace of X; coherence for b1 being non empty SubSpace of X st b1 is maximal_discrete holds not b1 is trivial proof let X0 be non empty SubSpace of X; ::_thesis: ( X0 is maximal_discrete implies not X0 is trivial ) reconsider A = the carrier of X0 as non empty Subset of X by Lm1; assume X0 is maximal_discrete ; ::_thesis: not X0 is trivial then A is maximal_discrete by Def6; then A is dense by Th56; then A1: Cl A = the carrier of X by TOPS_3:def_2; assume X0 is trivial ; ::_thesis: contradiction then consider s being Element of X0 such that A2: the carrier of X0 = {s} by SUBSET_1:46; s in A ; then reconsider a = s as Point of X ; A = {a} by A2; then for C being Subset of X for x being Point of X st C = {x} holds Cl C = the carrier of X by A1, Th49; hence contradiction by TDLAT_3:20; ::_thesis: verum end; cluster non empty trivial -> non empty non maximal_discrete for SubSpace of X; coherence for b1 being non empty SubSpace of X st b1 is trivial holds not b1 is maximal_discrete ; end; registration let X be non empty almost_discrete TopSpace; cluster non empty strict TopSpace-like maximal_discrete for SubSpace of X; existence ex b1 being SubSpace of X st ( b1 is maximal_discrete & b1 is strict & not b1 is empty & not b1 is empty ) proof consider M being Subset of X such that A1: M is maximal_discrete by Th60; not M is empty by A1, Th40; then consider X0 being non empty strict SubSpace of X such that A2: X0 is maximal_discrete and M = the carrier of X0 by A1, Th47; take X0 ; ::_thesis: ( X0 is maximal_discrete & X0 is strict & not X0 is empty & not X0 is empty ) thus ( X0 is maximal_discrete & X0 is strict & not X0 is empty & not X0 is empty ) by A2; ::_thesis: verum end; end; begin theorem Th62: :: TEX_2:62 for X being discrete TopSpace for Y being TopSpace for f being Function of X,Y holds f is continuous proof let X be discrete TopSpace; ::_thesis: for Y being TopSpace for f being Function of X,Y holds f is continuous let Y be TopSpace; ::_thesis: for f being Function of X,Y holds f is continuous let f be Function of X,Y; ::_thesis: f is continuous for B being Subset of Y st B is closed holds f " B is closed by TDLAT_3:16; hence f is continuous by PRE_TOPC:def_6; ::_thesis: verum end; theorem :: TEX_2:63 for X being non empty TopSpace st ( for Y being non empty TopSpace for f being Function of X,Y holds f is continuous ) holds X is discrete proof let X be non empty TopSpace; ::_thesis: ( ( for Y being non empty TopSpace for f being Function of X,Y holds f is continuous ) implies X is discrete ) set Y = 1TopSp the carrier of X; reconsider f = id the carrier of X as Function of X,(1TopSp the carrier of X) ; assume for Y being non empty TopSpace for f being Function of X,Y holds f is continuous ; ::_thesis: X is discrete then A1: f is continuous ; for A being Subset of X holds A is closed proof let A be Subset of X; ::_thesis: A is closed reconsider B = A as Subset of (1TopSp the carrier of X) ; A2: f " B = A by FUNCT_2:94; B is closed by TDLAT_3:16; hence A is closed by A1, A2, PRE_TOPC:def_6; ::_thesis: verum end; hence X is discrete by TDLAT_3:16; ::_thesis: verum end; theorem :: TEX_2:64 for X being non empty TopSpace for Y being non empty anti-discrete TopSpace for f being Function of X,Y holds f is continuous proof let X be non empty TopSpace; ::_thesis: for Y being non empty anti-discrete TopSpace for f being Function of X,Y holds f is continuous let Y be non empty anti-discrete TopSpace; ::_thesis: for f being Function of X,Y holds f is continuous let f be Function of X,Y; ::_thesis: f is continuous now__::_thesis:_for_B_being_Subset_of_Y_st_B_is_closed_holds_ f_"_B_is_closed let B be Subset of Y; ::_thesis: ( B is closed implies f " B is closed ) assume A1: B is closed ; ::_thesis: f " B is closed now__::_thesis:_f_"_B_is_closed percases ( B = {} or B = the carrier of Y ) by A1, TDLAT_3:19; suppose B = {} ; ::_thesis: f " B is closed then f " B = {} X ; hence f " B is closed ; ::_thesis: verum end; suppose B = the carrier of Y ; ::_thesis: f " B is closed then B = [#] Y ; then f " B = [#] X by TOPS_2:41; hence f " B is closed ; ::_thesis: verum end; end; end; hence f " B is closed ; ::_thesis: verum end; hence f is continuous by PRE_TOPC:def_6; ::_thesis: verum end; theorem :: TEX_2:65 for Y being non empty TopSpace st ( for X being non empty TopSpace for f being Function of X,Y holds f is continuous ) holds Y is anti-discrete proof let Y be non empty TopSpace; ::_thesis: ( ( for X being non empty TopSpace for f being Function of X,Y holds f is continuous ) implies Y is anti-discrete ) set X = ADTS the carrier of Y; A1: ADTS the carrier of Y = TopStruct(# the carrier of Y,(cobool the carrier of Y) #) by TEX_1:def_3; then reconsider f = id the carrier of Y as Function of (ADTS the carrier of Y),Y ; assume for X being non empty TopSpace for f being Function of X,Y holds f is continuous ; ::_thesis: Y is anti-discrete then A2: f is continuous ; for A being Subset of Y holds ( not A is closed or A = {} or A = the carrier of Y ) proof let A be Subset of Y; ::_thesis: ( not A is closed or A = {} or A = the carrier of Y ) reconsider B = A as Subset of (ADTS the carrier of Y) by A1; A3: f " A = B by FUNCT_2:94; assume A is closed ; ::_thesis: ( A = {} or A = the carrier of Y ) then B is closed by A2, A3, PRE_TOPC:def_6; hence ( A = {} or A = the carrier of Y ) by A1, TDLAT_3:19; ::_thesis: verum end; hence Y is anti-discrete by TDLAT_3:19; ::_thesis: verum end; theorem Th66: :: TEX_2:66 for X being non empty discrete TopSpace for X0 being non empty SubSpace of X ex r being continuous Function of X,X0 st r is being_a_retraction proof let X be non empty discrete TopSpace; ::_thesis: for X0 being non empty SubSpace of X ex r being continuous Function of X,X0 st r is being_a_retraction let X0 be non empty SubSpace of X; ::_thesis: ex r being continuous Function of X,X0 st r is being_a_retraction reconsider A = the carrier of X0 as Subset of X by TSEP_1:1; defpred S1[ set , set ] means ( $1 in A implies $2 = $1 ); A1: for x being Point of X ex a being Point of X0 st S1[x,a] ; consider r being Function of X,X0 such that A2: for x being Point of X holds S1[x,r . x] from FUNCT_2:sch_3(A1); reconsider r = r as continuous Function of X,X0 by Th62; take r ; ::_thesis: r is being_a_retraction thus r is being_a_retraction by A2, BORSUK_1:def_16; ::_thesis: verum end; theorem :: TEX_2:67 for X being non empty discrete TopSpace for X0 being non empty SubSpace of X holds X0 is_a_retract_of X proof let X be non empty discrete TopSpace; ::_thesis: for X0 being non empty SubSpace of X holds X0 is_a_retract_of X let X0 be non empty SubSpace of X; ::_thesis: X0 is_a_retract_of X ex r being continuous Function of X,X0 st r is being_a_retraction by Th66; hence X0 is_a_retract_of X by BORSUK_1:def_17; ::_thesis: verum end; theorem Th68: :: TEX_2:68 for X being non empty almost_discrete TopSpace for X0 being non empty maximal_discrete SubSpace of X ex r being continuous Function of X,X0 st r is being_a_retraction proof let X be non empty almost_discrete TopSpace; ::_thesis: for X0 being non empty maximal_discrete SubSpace of X ex r being continuous Function of X,X0 st r is being_a_retraction let X0 be non empty maximal_discrete SubSpace of X; ::_thesis: ex r being continuous Function of X,X0 st r is being_a_retraction reconsider A = the carrier of X0 as Subset of X by TSEP_1:1; defpred S1[ Point of X, Point of X0] means A /\ (Cl {$1}) = {$2}; A1: A is maximal_discrete by Th45; then A2: A is discrete by Def5; A3: for x being Point of X ex a being Point of X0 st S1[x,a] proof let x be Point of X; ::_thesis: ex a being Point of X0 st S1[x,a] consider a being Point of X such that A4: a in A and A5: A /\ (Cl {x}) = {a} by A1, Th58; reconsider a = a as Point of X0 by A4; take a ; ::_thesis: S1[x,a] thus S1[x,a] by A5; ::_thesis: verum end; consider r being Function of X,X0 such that A6: for x being Point of X holds S1[x,r . x] from FUNCT_2:sch_3(A3); for F being Subset of X0 st F is closed holds r " F is closed proof let F be Subset of X0; ::_thesis: ( F is closed implies r " F is closed ) assume F is closed ; ::_thesis: r " F is closed F c= A ; then reconsider E = F as Subset of X by XBOOLE_1:1; set R = { (Cl {a}) where a is Point of X : a in E } ; now__::_thesis:_for_x_being_set_st_x_in_r_"_F_holds_ x_in_union__{__(Cl_{a})_where_a_is_Point_of_X_:_a_in_E__}_ let x be set ; ::_thesis: ( x in r " F implies x in union { (Cl {a}) where a is Point of X : a in E } ) assume A7: x in r " F ; ::_thesis: x in union { (Cl {a}) where a is Point of X : a in E } then reconsider b = x as Point of X ; A8: r . b in F by A7, FUNCT_2:38; E c= the carrier of X ; then reconsider a = r . b as Point of X by A8; Cl {a} in { (Cl {a}) where a is Point of X : a in E } by A8; then A9: Cl {a} c= union { (Cl {a}) where a is Point of X : a in E } by ZFMISC_1:74; A /\ (Cl {b}) = {a} by A6; then a in A /\ (Cl {b}) by ZFMISC_1:31; then a in Cl {b} by XBOOLE_0:def_4; then A10: Cl {a} = Cl {b} by Th49; A11: {b} c= Cl {b} by PRE_TOPC:18; b in {b} by TARSKI:def_1; then b in Cl {a} by A10, A11; hence x in union { (Cl {a}) where a is Point of X : a in E } by A9; ::_thesis: verum end; then A12: r " F c= union { (Cl {a}) where a is Point of X : a in E } by TARSKI:def_3; now__::_thesis:_for_C_being_set_st_C_in__{__(Cl_{a})_where_a_is_Point_of_X_:_a_in_E__}__holds_ C_c=_r_"_F let C be set ; ::_thesis: ( C in { (Cl {a}) where a is Point of X : a in E } implies C c= r " F ) assume C in { (Cl {a}) where a is Point of X : a in E } ; ::_thesis: C c= r " F then consider a being Point of X such that A13: C = Cl {a} and A14: a in E ; now__::_thesis:_for_x_being_set_st_x_in_C_holds_ x_in_r_"_F let x be set ; ::_thesis: ( x in C implies x in r " F ) assume A15: x in C ; ::_thesis: x in r " F then reconsider b = x as Point of X by A13; A16: A /\ (Cl {b}) = {(r . b)} by A6; A17: A /\ (Cl {a}) = {a} by A2, A14, Th36; Cl {a} = Cl {b} by A13, A15, Th49; then a = r . x by A17, A16, ZFMISC_1:3; hence x in r " F by A13, A14, A15, FUNCT_2:38; ::_thesis: verum end; hence C c= r " F by TARSKI:def_3; ::_thesis: verum end; then A18: union { (Cl {a}) where a is Point of X : a in E } c= r " F by ZFMISC_1:76; Cl E = union { (Cl {a}) where a is Point of X : a in E } by Th48; hence r " F is closed by A18, A12, XBOOLE_0:def_10; ::_thesis: verum end; then reconsider r = r as continuous Function of X,X0 by PRE_TOPC:def_6; take r ; ::_thesis: r is being_a_retraction for x being Point of X st x in the carrier of X0 holds r . x = x proof let x be Point of X; ::_thesis: ( x in the carrier of X0 implies r . x = x ) assume x in the carrier of X0 ; ::_thesis: r . x = x then A19: A /\ (Cl {x}) = {x} by A2, Th36; A /\ (Cl {x}) = {(r . x)} by A6; hence r . x = x by A19, ZFMISC_1:3; ::_thesis: verum end; hence r is being_a_retraction by BORSUK_1:def_16; ::_thesis: verum end; theorem :: TEX_2:69 for X being non empty almost_discrete TopSpace for X0 being non empty maximal_discrete SubSpace of X holds X0 is_a_retract_of X proof let X be non empty almost_discrete TopSpace; ::_thesis: for X0 being non empty maximal_discrete SubSpace of X holds X0 is_a_retract_of X let X0 be non empty maximal_discrete SubSpace of X; ::_thesis: X0 is_a_retract_of X ex r being continuous Function of X,X0 st r is being_a_retraction by Th68; hence X0 is_a_retract_of X by BORSUK_1:def_17; ::_thesis: verum end; Lm4: for X being non empty almost_discrete TopSpace for X0 being non empty maximal_discrete SubSpace of X for r being continuous Function of X,X0 st r is being_a_retraction holds for a being Point of X0 for b being Point of X st a = b holds Cl {b} c= r " {a} proof let X be non empty almost_discrete TopSpace; ::_thesis: for X0 being non empty maximal_discrete SubSpace of X for r being continuous Function of X,X0 st r is being_a_retraction holds for a being Point of X0 for b being Point of X st a = b holds Cl {b} c= r " {a} let X0 be non empty maximal_discrete SubSpace of X; ::_thesis: for r being continuous Function of X,X0 st r is being_a_retraction holds for a being Point of X0 for b being Point of X st a = b holds Cl {b} c= r " {a} let r be continuous Function of X,X0; ::_thesis: ( r is being_a_retraction implies for a being Point of X0 for b being Point of X st a = b holds Cl {b} c= r " {a} ) assume A1: r is being_a_retraction ; ::_thesis: for a being Point of X0 for b being Point of X st a = b holds Cl {b} c= r " {a} let a be Point of X0; ::_thesis: for b being Point of X st a = b holds Cl {b} c= r " {a} let b be Point of X; ::_thesis: ( a = b implies Cl {b} c= r " {a} ) assume a = b ; ::_thesis: Cl {b} c= r " {a} then A2: r . b = a by A1, BORSUK_1:def_16; a in {a} by TARSKI:def_1; then b in r " {a} by A2, FUNCT_2:38; then A3: {b} c= r " {a} by ZFMISC_1:31; {a} is closed by TDLAT_3:16; then r " {a} is closed by PRE_TOPC:def_6; hence Cl {b} c= r " {a} by A3, TOPS_1:5; ::_thesis: verum end; theorem Th70: :: TEX_2:70 for X being non empty almost_discrete TopSpace for X0 being non empty maximal_discrete SubSpace of X for r being continuous Function of X,X0 st r is being_a_retraction holds for F being Subset of X0 for E being Subset of X st F = E holds r " F = Cl E proof let X be non empty almost_discrete TopSpace; ::_thesis: for X0 being non empty maximal_discrete SubSpace of X for r being continuous Function of X,X0 st r is being_a_retraction holds for F being Subset of X0 for E being Subset of X st F = E holds r " F = Cl E let X0 be non empty maximal_discrete SubSpace of X; ::_thesis: for r being continuous Function of X,X0 st r is being_a_retraction holds for F being Subset of X0 for E being Subset of X st F = E holds r " F = Cl E let r be continuous Function of X,X0; ::_thesis: ( r is being_a_retraction implies for F being Subset of X0 for E being Subset of X st F = E holds r " F = Cl E ) reconsider A = the carrier of X0 as Subset of X by TSEP_1:1; A1: A is maximal_discrete by Th45; assume A2: r is being_a_retraction ; ::_thesis: for F being Subset of X0 for E being Subset of X st F = E holds r " F = Cl E A3: for a being Point of X holds A /\ (Cl {a}) = {(r . a)} proof let a be Point of X; ::_thesis: A /\ (Cl {a}) = {(r . a)} A4: {a} c= Cl {a} by PRE_TOPC:18; consider c being Point of X such that A5: c in A and A6: A /\ (Cl {a}) = {c} by A1, Th58; reconsider b = c as Point of X0 by A5; {c} c= Cl {a} by A6, XBOOLE_1:17; then A7: c in Cl {a} by ZFMISC_1:31; Cl {c} c= r " {b} by A2, Lm4; then Cl {a} c= r " {b} by A7, Th49; then {a} c= r " {b} by A4, XBOOLE_1:1; then a in r " {b} by ZFMISC_1:31; then r . a in {b} by FUNCT_2:38; hence A /\ (Cl {a}) = {(r . a)} by A6, TARSKI:def_1; ::_thesis: verum end; let F be Subset of X0; ::_thesis: for E being Subset of X st F = E holds r " F = Cl E let E be Subset of X; ::_thesis: ( F = E implies r " F = Cl E ) set R = { (Cl {a}) where a is Point of X : a in E } ; assume A8: F = E ; ::_thesis: r " F = Cl E now__::_thesis:_for_x_being_set_st_x_in_r_"_F_holds_ x_in_union__{__(Cl_{a})_where_a_is_Point_of_X_:_a_in_E__}_ let x be set ; ::_thesis: ( x in r " F implies x in union { (Cl {a}) where a is Point of X : a in E } ) assume A9: x in r " F ; ::_thesis: x in union { (Cl {a}) where a is Point of X : a in E } then reconsider b = x as Point of X ; A10: r . b in F by A9, FUNCT_2:38; then reconsider a = r . b as Point of X by A8; Cl {a} in { (Cl {a}) where a is Point of X : a in E } by A8, A10; then A11: Cl {a} c= union { (Cl {a}) where a is Point of X : a in E } by ZFMISC_1:74; A12: {b} c= Cl {b} by PRE_TOPC:18; A /\ (Cl {b}) = {a} by A3; then a in A /\ (Cl {b}) by ZFMISC_1:31; then a in Cl {b} by XBOOLE_0:def_4; then A13: Cl {a} = Cl {b} by Th49; b in {b} by TARSKI:def_1; then b in Cl {a} by A13, A12; hence x in union { (Cl {a}) where a is Point of X : a in E } by A11; ::_thesis: verum end; then A14: r " F c= union { (Cl {a}) where a is Point of X : a in E } by TARSKI:def_3; A15: A is discrete by A1, Def5; now__::_thesis:_for_C_being_set_st_C_in__{__(Cl_{a})_where_a_is_Point_of_X_:_a_in_E__}__holds_ C_c=_r_"_F let C be set ; ::_thesis: ( C in { (Cl {a}) where a is Point of X : a in E } implies C c= r " F ) assume C in { (Cl {a}) where a is Point of X : a in E } ; ::_thesis: C c= r " F then consider a being Point of X such that A16: C = Cl {a} and A17: a in E ; now__::_thesis:_for_x_being_set_st_x_in_C_holds_ x_in_r_"_F let x be set ; ::_thesis: ( x in C implies x in r " F ) assume A18: x in C ; ::_thesis: x in r " F then reconsider b = x as Point of X by A16; A19: A /\ (Cl {b}) = {(r . b)} by A3; A20: A /\ (Cl {a}) = {a} by A8, A15, A17, Th36; Cl {a} = Cl {b} by A16, A18, Th49; then a = r . x by A20, A19, ZFMISC_1:3; hence x in r " F by A8, A16, A17, A18, FUNCT_2:38; ::_thesis: verum end; hence C c= r " F by TARSKI:def_3; ::_thesis: verum end; then A21: union { (Cl {a}) where a is Point of X : a in E } c= r " F by ZFMISC_1:76; Cl E = union { (Cl {a}) where a is Point of X : a in E } by Th48; hence r " F = Cl E by A21, A14, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: TEX_2:71 for X being non empty almost_discrete TopSpace for X0 being non empty maximal_discrete SubSpace of X for r being continuous Function of X,X0 st r is being_a_retraction holds for a being Point of X0 for b being Point of X st a = b holds r " {a} = Cl {b} by Th70; theorem Th72: :: TEX_2:72 for X being non empty almost_discrete TopSpace for X0 being non empty discrete SubSpace of X ex r being continuous Function of X,X0 st r is being_a_retraction proof let X be non empty almost_discrete TopSpace; ::_thesis: for X0 being non empty discrete SubSpace of X ex r being continuous Function of X,X0 st r is being_a_retraction let X0 be non empty discrete SubSpace of X; ::_thesis: ex r being continuous Function of X,X0 st r is being_a_retraction consider Z0 being non empty strict SubSpace of X such that A1: X0 is SubSpace of Z0 and A2: Z0 is maximal_discrete by Th61; reconsider Z0 = Z0 as non empty strict maximal_discrete SubSpace of X by A2; reconsider Z1 = Z0 as non empty TopSpace ; reconsider Z1 = Z1 as non empty discrete TopSpace ; reconsider X1 = X0 as non empty SubSpace of Z1 by A1; consider g being continuous Function of Z1,X1 such that A3: g is being_a_retraction by Th66; reconsider g = g as continuous Function of Z0,X0 ; consider h being continuous Function of X,Z0 such that A4: h is being_a_retraction by Th68; reconsider r = g * h as continuous Function of X,X0 ; take r ; ::_thesis: r is being_a_retraction for x being Point of X st x in the carrier of X0 holds r . x = x proof let x be Point of X; ::_thesis: ( x in the carrier of X0 implies r . x = x ) assume A5: x in the carrier of X0 ; ::_thesis: r . x = x the carrier of X1 c= the carrier of Z1 by BORSUK_1:1; then reconsider y = x as Point of Z1 by A5; g . y = y by A3, A5, BORSUK_1:def_16; then g . (h . x) = x by A4, BORSUK_1:def_16; hence r . x = x by FUNCT_2:15; ::_thesis: verum end; hence r is being_a_retraction by BORSUK_1:def_16; ::_thesis: verum end; theorem :: TEX_2:73 for X being non empty almost_discrete TopSpace for X0 being non empty discrete SubSpace of X holds X0 is_a_retract_of X proof let X be non empty almost_discrete TopSpace; ::_thesis: for X0 being non empty discrete SubSpace of X holds X0 is_a_retract_of X let X0 be non empty discrete SubSpace of X; ::_thesis: X0 is_a_retract_of X ex r being continuous Function of X,X0 st r is being_a_retraction by Th72; hence X0 is_a_retract_of X by BORSUK_1:def_17; ::_thesis: verum end;