:: TEX_1 semantic presentation begin theorem Th1: :: TEX_1:1 for X being non empty TopSpace for D, B being Subset of X for C being Subset of (X modified_with_respect_to D) st B = C & B is open holds C is open proof let X be non empty TopSpace; ::_thesis: for D, B being Subset of X for C being Subset of (X modified_with_respect_to D) st B = C & B is open holds C is open let D, B be Subset of X; ::_thesis: for C being Subset of (X modified_with_respect_to D) st B = C & B is open holds C is open let C be Subset of (X modified_with_respect_to D); ::_thesis: ( B = C & B is open implies C is open ) assume A1: B = C ; ::_thesis: ( not B is open or C is open ) A2: the topology of X c= D -extension_of_the_topology_of X by TMAP_1:88; A3: the topology of (X modified_with_respect_to D) = D -extension_of_the_topology_of X by TMAP_1:93; assume B in the topology of X ; :: according to PRE_TOPC:def_2 ::_thesis: C is open hence C is open by A1, A2, A3, PRE_TOPC:def_2; ::_thesis: verum end; theorem :: TEX_1:2 for X being non empty TopSpace for D, B being Subset of X for C being Subset of (X modified_with_respect_to D) st B = C & B is closed holds C is closed proof let X be non empty TopSpace; ::_thesis: for D, B being Subset of X for C being Subset of (X modified_with_respect_to D) st B = C & B is closed holds C is closed let D, B be Subset of X; ::_thesis: for C being Subset of (X modified_with_respect_to D) st B = C & B is closed holds C is closed let C be Subset of (X modified_with_respect_to D); ::_thesis: ( B = C & B is closed implies C is closed ) assume A1: B = C ; ::_thesis: ( not B is closed or C is closed ) A2: the carrier of (X modified_with_respect_to D) = the carrier of X by TMAP_1:93; assume B is closed ; ::_thesis: C is closed then C ` is open by A1, A2, Th1; hence C is closed by TOPS_1:3; ::_thesis: verum end; theorem Th3: :: TEX_1:3 for X being non empty TopSpace for D being Subset of X for C being Subset of (X modified_with_respect_to (D `)) st C = D holds C is closed proof let X be non empty TopSpace; ::_thesis: for D being Subset of X for C being Subset of (X modified_with_respect_to (D `)) st C = D holds C is closed let D be Subset of X; ::_thesis: for C being Subset of (X modified_with_respect_to (D `)) st C = D holds C is closed let C be Subset of (X modified_with_respect_to (D `)); ::_thesis: ( C = D implies C is closed ) assume C = D ; ::_thesis: C is closed then C ` = D ` by TMAP_1:93; then C ` is open by TMAP_1:94; hence C is closed by TOPS_1:3; ::_thesis: verum end; theorem Th4: :: TEX_1:4 for X being non empty TopSpace for D being Subset of X for C being Subset of (X modified_with_respect_to D) st C = D & D is dense holds ( C is dense & C is open ) proof let X be non empty TopSpace; ::_thesis: for D being Subset of X for C being Subset of (X modified_with_respect_to D) st C = D & D is dense holds ( C is dense & C is open ) let D be Subset of X; ::_thesis: for C being Subset of (X modified_with_respect_to D) st C = D & D is dense holds ( C is dense & C is open ) let C be Subset of (X modified_with_respect_to D); ::_thesis: ( C = D & D is dense implies ( C is dense & C is open ) ) assume A1: C = D ; ::_thesis: ( not D is dense or ( C is dense & C is open ) ) set A = (Cl C) ` ; (Cl C) ` in the topology of (X modified_with_respect_to D) by PRE_TOPC:def_2; then (Cl C) ` in D -extension_of_the_topology_of X by TMAP_1:93; then A2: (Cl C) ` in { (H \/ (G /\ D)) where H, G is Subset of X : ( H in the topology of X & G in the topology of X ) } by TMAP_1:def_7; reconsider B = (Cl C) ` as Subset of X by TMAP_1:93; consider H, G being Subset of X such that A3: (Cl C) ` = H \/ (G /\ D) and A4: H in the topology of X and G in the topology of X by A2; A5: H c= (Cl C) ` by A3, XBOOLE_1:7; A6: C c= Cl C by PRE_TOPC:18; then D misses (Cl C) ` by A1, SUBSET_1:24; then G /\ D misses (Cl C) ` by XBOOLE_1:17, XBOOLE_1:63; then A7: (G /\ D) /\ ((Cl C) `) = {} by XBOOLE_0:def_7; (Cl C) ` = (H \/ (G /\ D)) /\ ((Cl C) `) by A3 .= (H /\ ((Cl C) `)) \/ {} by A7, XBOOLE_1:23 .= H /\ ((Cl C) `) ; then (Cl C) ` c= H by XBOOLE_1:17; then B = H by A5, XBOOLE_0:def_10; then A8: B is open by A4, PRE_TOPC:def_2; D misses B by A1, A6, SUBSET_1:24; then Cl D misses B by A8, TSEP_1:36; then A9: (Cl D) /\ B = {} by XBOOLE_0:def_7; assume D is dense ; ::_thesis: ( C is dense & C is open ) then A10: Cl D = [#] X by TOPS_1:def_3; thus C is dense ::_thesis: C is open proof assume not C is dense ; ::_thesis: contradiction then Cl C <> [#] (X modified_with_respect_to D) by TOPS_1:def_3; then B <> {} (X modified_with_respect_to D) by TOPS_3:2; hence contradiction by A9, A10, XBOOLE_1:28; ::_thesis: verum end; thus C is open by A1, TMAP_1:94; ::_thesis: verum end; theorem Th5: :: TEX_1:5 for X being non empty TopSpace for D being Subset of X for C being Subset of (X modified_with_respect_to D) st D c= C & D is dense holds C is everywhere_dense proof let X be non empty TopSpace; ::_thesis: for D being Subset of X for C being Subset of (X modified_with_respect_to D) st D c= C & D is dense holds C is everywhere_dense let D be Subset of X; ::_thesis: for C being Subset of (X modified_with_respect_to D) st D c= C & D is dense holds C is everywhere_dense let C be Subset of (X modified_with_respect_to D); ::_thesis: ( D c= C & D is dense implies C is everywhere_dense ) assume A1: D c= C ; ::_thesis: ( not D is dense or C is everywhere_dense ) reconsider E = D as Subset of (X modified_with_respect_to D) by TMAP_1:93; assume A2: D is dense ; ::_thesis: C is everywhere_dense then A3: E is open by Th4; E is dense by A2, Th4; hence C is everywhere_dense by A1, A3, TOPS_3:36, TOPS_3:38; ::_thesis: verum end; theorem Th6: :: TEX_1:6 for X being non empty TopSpace for D being Subset of X for C being Subset of (X modified_with_respect_to (D `)) st C = D & D is boundary holds ( C is boundary & C is closed ) proof let X be non empty TopSpace; ::_thesis: for D being Subset of X for C being Subset of (X modified_with_respect_to (D `)) st C = D & D is boundary holds ( C is boundary & C is closed ) let D be Subset of X; ::_thesis: for C being Subset of (X modified_with_respect_to (D `)) st C = D & D is boundary holds ( C is boundary & C is closed ) let C be Subset of (X modified_with_respect_to (D `)); ::_thesis: ( C = D & D is boundary implies ( C is boundary & C is closed ) ) assume C = D ; ::_thesis: ( not D is boundary or ( C is boundary & C is closed ) ) then A1: C ` = D ` by TMAP_1:93; assume D is boundary ; ::_thesis: ( C is boundary & C is closed ) then A2: D ` is dense by TOPS_1:def_4; then A3: C ` is open by A1, Th4; C ` is dense by A1, A2, Th4; hence ( C is boundary & C is closed ) by A3, TOPS_1:3, TOPS_1:def_4; ::_thesis: verum end; theorem Th7: :: TEX_1:7 for X being non empty TopSpace for D being Subset of X for C being Subset of (X modified_with_respect_to (D `)) st C c= D & D is boundary holds C is nowhere_dense proof let X be non empty TopSpace; ::_thesis: for D being Subset of X for C being Subset of (X modified_with_respect_to (D `)) st C c= D & D is boundary holds C is nowhere_dense let D be Subset of X; ::_thesis: for C being Subset of (X modified_with_respect_to (D `)) st C c= D & D is boundary holds C is nowhere_dense let C be Subset of (X modified_with_respect_to (D `)); ::_thesis: ( C c= D & D is boundary implies C is nowhere_dense ) assume A1: C c= D ; ::_thesis: ( not D is boundary or C is nowhere_dense ) reconsider E = D as Subset of (X modified_with_respect_to (D `)) by TMAP_1:93; assume A2: D is boundary ; ::_thesis: C is nowhere_dense then A3: E is closed by Th6; E is boundary by A2, Th6; hence C is nowhere_dense by A1, A3, TOPS_3:26; ::_thesis: verum end; Lm1: for X, Y being set holds ( X c= Y iff X is Subset of Y ) ; begin definition let Y be non empty 1-sorted ; redefine attr Y is trivial means :Def1: :: TEX_1:def 1 ex d being Element of Y st the carrier of Y = {d}; compatibility ( Y is trivial iff ex d being Element of Y st the carrier of Y = {d} ) proof hereby ::_thesis: ( ex d being Element of Y st the carrier of Y = {d} implies Y is trivial ) assume A1: Y is trivial ; ::_thesis: ex d being Element of Y st the carrier of Y = {d} thus ex d being Element of Y st the carrier of Y = {d} ::_thesis: verum proof reconsider A = the carrier of Y as Subset of Y by Lm1; set d = the Element of Y; reconsider D = { the Element of Y} as Subset of Y ; take the Element of Y ; ::_thesis: the carrier of Y = { the Element of Y} now__::_thesis:_for_a_being_Element_of_Y_st_a_in_A_holds_ a_in_D let a be Element of Y; ::_thesis: ( a in A implies a in D ) assume a in A ; ::_thesis: a in D a = the Element of Y by A1, STRUCT_0:def_10; hence a in D by TARSKI:def_1; ::_thesis: verum end; then A c= D by SUBSET_1:2; hence the carrier of Y = { the Element of Y} by XBOOLE_0:def_10; ::_thesis: verum end; end; given d being Element of Y such that A2: the carrier of Y = {d} ; ::_thesis: Y is trivial now__::_thesis:_for_a,_b_being_Element_of_Y_holds_a_=_b let a, b be Element of Y; ::_thesis: a = b a = d by A2, TARSKI:def_1; hence a = b by A2, TARSKI:def_1; ::_thesis: verum end; hence Y is trivial by STRUCT_0:def_10; ::_thesis: verum end; end; :: deftheorem Def1 defines trivial TEX_1:def_1_:_ for Y being non empty 1-sorted holds ( Y is trivial iff ex d being Element of Y st the carrier of Y = {d} ); registration cluster1 -element strict for TopStruct ; existence ex b1 being TopStruct st ( b1 is 1 -element & b1 is strict ) proof set O = the 1 -element 1-sorted ; reconsider tau = {} as Subset-Family of the 1 -element 1-sorted by XBOOLE_1:2; reconsider tau = tau as Subset-Family of the 1 -element 1-sorted ; take TopStruct(# the carrier of the 1 -element 1-sorted ,tau #) ; ::_thesis: ( TopStruct(# the carrier of the 1 -element 1-sorted ,tau #) is 1 -element & TopStruct(# the carrier of the 1 -element 1-sorted ,tau #) is strict ) thus the carrier of TopStruct(# the carrier of the 1 -element 1-sorted ,tau #) is 1 -element ; :: according to STRUCT_0:def_19 ::_thesis: TopStruct(# the carrier of the 1 -element 1-sorted ,tau #) is strict thus TopStruct(# the carrier of the 1 -element 1-sorted ,tau #) is strict ; ::_thesis: verum end; cluster non trivial strict for TopStruct ; existence ex b1 being TopStruct st ( not b1 is trivial & b1 is strict ) proof set O = the non trivial 1-sorted ; reconsider tau = {} as Subset-Family of the non trivial 1-sorted by XBOOLE_1:2; take TopStruct(# the carrier of the non trivial 1-sorted ,tau #) ; ::_thesis: ( not TopStruct(# the carrier of the non trivial 1-sorted ,tau #) is trivial & TopStruct(# the carrier of the non trivial 1-sorted ,tau #) is strict ) thus ( not TopStruct(# the carrier of the non trivial 1-sorted ,tau #) is trivial & TopStruct(# the carrier of the non trivial 1-sorted ,tau #) is strict ) ; ::_thesis: verum end; end; theorem :: TEX_1:8 for Y being 1 -element TopStruct st not the topology of Y is empty & Y is almost_discrete holds Y is TopSpace-like proof let Y be 1 -element TopStruct ; ::_thesis: ( not the topology of Y is empty & Y is almost_discrete implies Y is TopSpace-like ) consider d being Element of Y such that A1: the carrier of Y = {d} by Def1; reconsider D = {d} as Subset of Y ; assume not the topology of Y is empty ; ::_thesis: ( not Y is almost_discrete or Y is TopSpace-like ) then consider A being Subset of Y such that A2: A in the topology of Y by SUBSET_1:4; assume A3: for A being Subset of Y st A in the topology of Y holds the carrier of Y \ A in the topology of Y ; :: according to TDLAT_3:def_3 ::_thesis: Y is TopSpace-like A4: bool D = {{},D} by ZFMISC_1:24; now__::_thesis:_{{},D}_c=_the_topology_of_Y percases ( A = {} or A = D ) by A1, A4, TARSKI:def_2; supposeA5: A = {} ; ::_thesis: {{},D} c= the topology of Y D \ A in the topology of Y by A1, A2, A3; hence {{},D} c= the topology of Y by A2, A5, ZFMISC_1:32; ::_thesis: verum end; supposeA6: A = D ; ::_thesis: {{},D} c= the topology of Y D \ A in the topology of Y by A1, A2, A3; then {} in the topology of Y by A6, XBOOLE_1:37; hence {{},D} c= the topology of Y by A2, A6, ZFMISC_1:32; ::_thesis: verum end; end; end; then the topology of Y = {{}, the carrier of Y} by A1, A4, XBOOLE_0:def_10; then reconsider Y = Y as anti-discrete TopStruct by TDLAT_3:def_2; Y is TopSpace-like ; hence Y is TopSpace-like ; ::_thesis: verum end; registration cluster1 -element strict TopSpace-like for TopStruct ; existence ex b1 being TopSpace st ( b1 is 1 -element & b1 is strict ) proof set O = the 1 -element 1-sorted ; reconsider tau = bool the carrier of the 1 -element 1-sorted as Subset-Family of the 1 -element 1-sorted ; set Y = TopStruct(# the carrier of the 1 -element 1-sorted ,tau #); reconsider Y = TopStruct(# the carrier of the 1 -element 1-sorted ,tau #) as non empty discrete TopStruct by TDLAT_3:def_1; reconsider Y = Y as non empty TopSpace-like TopStruct ; take Y ; ::_thesis: ( Y is 1 -element & Y is strict ) thus the carrier of Y is 1 -element ; :: according to STRUCT_0:def_19 ::_thesis: Y is strict thus Y is strict ; ::_thesis: verum end; end; registration cluster1 -element TopSpace-like -> 1 -element discrete anti-discrete for TopStruct ; coherence for b1 being 1 -element TopSpace holds ( b1 is anti-discrete & b1 is discrete ) proof let Y be 1 -element TopSpace; ::_thesis: ( Y is anti-discrete & Y is discrete ) A1: the carrier of Y in the topology of Y by PRE_TOPC:def_1; ex d being Element of Y st the carrier of Y = {d} by Def1; then A2: bool the carrier of Y = {{}, the carrier of Y} by ZFMISC_1:24; {} in the topology of Y by PRE_TOPC:1; then {{}, the carrier of Y} c= the topology of Y by A1, ZFMISC_1:32; then the topology of Y = bool the carrier of Y by A2, XBOOLE_0:def_10; hence ( Y is anti-discrete & Y is discrete ) by A2, TDLAT_3:def_1, TDLAT_3:def_2; ::_thesis: verum end; cluster non empty TopSpace-like discrete anti-discrete -> non empty trivial for TopStruct ; coherence for b1 being non empty TopSpace st b1 is discrete & b1 is anti-discrete holds b1 is trivial proof let Y be non empty TopSpace; ::_thesis: ( Y is discrete & Y is anti-discrete implies Y is trivial ) assume ( Y is discrete & Y is anti-discrete ) ; ::_thesis: Y is trivial then A3: bool the carrier of Y = {{}, the carrier of Y} by TDLAT_3:10; now__::_thesis:_ex_d0_being_Element_of_Y_st_{d0}_=_the_carrier_of_Y set d0 = the Element of Y; take d0 = the Element of Y; ::_thesis: {d0} = the carrier of Y thus {d0} = the carrier of Y by A3, TARSKI:def_2; ::_thesis: verum end; hence Y is trivial ; ::_thesis: verum end; end; registration cluster non trivial strict TopSpace-like for TopStruct ; existence ex b1 being TopSpace st ( not b1 is trivial & b1 is strict ) proof set D = {{},1}; reconsider tau = bool {{},1} as Subset-Family of {{},1} ; reconsider tau = tau as Subset-Family of {{},1} ; reconsider Y = TopStruct(# {{},1},tau #) as non empty discrete TopStruct by TDLAT_3:def_1; take Y ; ::_thesis: ( not Y is trivial & Y is strict ) now__::_thesis:_not_Y_is_trivial assume Y is trivial ; ::_thesis: contradiction then consider d being Element of Y such that A1: the carrier of Y = {d} by Def1; d = {} by A1, ZFMISC_1:4; hence contradiction by A1, ZFMISC_1:4; ::_thesis: verum end; hence ( not Y is trivial & Y is strict ) ; ::_thesis: verum end; end; registration cluster non empty TopSpace-like non discrete -> non empty non trivial for TopStruct ; coherence for b1 being non empty TopSpace st not b1 is discrete holds not b1 is trivial proof let T be non empty TopSpace; ::_thesis: ( not T is discrete implies not T is trivial ) assume not T is discrete ; ::_thesis: not T is trivial then T is not 1 -element TopSpace ; then not the carrier of T is 1 -element by STRUCT_0:def_19; hence not T is trivial ; ::_thesis: verum end; cluster non empty TopSpace-like non anti-discrete -> non empty non trivial for TopStruct ; coherence for b1 being non empty TopSpace st not b1 is anti-discrete holds not b1 is trivial proof let T be non empty TopSpace; ::_thesis: ( not T is anti-discrete implies not T is trivial ) assume not T is anti-discrete ; ::_thesis: not T is trivial then T is not 1 -element TopSpace ; then not the carrier of T is 1 -element by STRUCT_0:def_19; hence not T is trivial ; ::_thesis: verum end; end; begin definition let D be set ; func cobool D -> Subset-Family of D equals :: TEX_1:def 2 {{},D}; coherence {{},D} is Subset-Family of D proof A1: D in bool D by ZFMISC_1:def_1; {} c= D by XBOOLE_1:2; hence {{},D} is Subset-Family of D by A1, ZFMISC_1:32; ::_thesis: verum end; end; :: deftheorem defines cobool TEX_1:def_2_:_ for D being set holds cobool D = {{},D}; registration let D be set ; cluster cobool D -> non empty ; coherence not cobool D is empty ; end; definition let D be set ; func ADTS D -> TopStruct equals :: TEX_1:def 3 TopStruct(# D,(cobool D) #); coherence TopStruct(# D,(cobool D) #) is TopStruct ; end; :: deftheorem defines ADTS TEX_1:def_3_:_ for D being set holds ADTS D = TopStruct(# D,(cobool D) #); registration let D be set ; cluster ADTS D -> strict TopSpace-like anti-discrete ; coherence ( ADTS D is strict & ADTS D is anti-discrete & ADTS D is TopSpace-like ) proof set Y = TopStruct(# D,(cobool D) #); reconsider Y9 = TopStruct(# D,(cobool D) #) as anti-discrete TopStruct by TDLAT_3:def_2; Y9 is strict anti-discrete TopSpace ; hence ( ADTS D is strict & ADTS D is anti-discrete & ADTS D is TopSpace-like ) ; ::_thesis: verum end; end; registration let D be non empty set ; cluster ADTS D -> non empty ; coherence not ADTS D is empty ; end; theorem Th9: :: TEX_1:9 for X being non empty anti-discrete TopSpace for A being Subset of X holds ( ( A is empty implies Cl A = {} ) & ( not A is empty implies Cl A = the carrier of X ) ) proof let X be non empty anti-discrete TopSpace; ::_thesis: for A being Subset of X holds ( ( A is empty implies Cl A = {} ) & ( not A is empty implies Cl A = the carrier of X ) ) let A be Subset of X; ::_thesis: ( ( A is empty implies Cl A = {} ) & ( not A is empty implies Cl A = the carrier of X ) ) thus ( A is empty implies Cl A = {} ) by PRE_TOPC:22; ::_thesis: ( not A is empty implies Cl A = the carrier of X ) thus ( not A is empty implies Cl A = the carrier of X ) ::_thesis: verum proof assume not A is empty ; ::_thesis: Cl A = the carrier of X then Cl A <> {} by PCOMPS_1:2; hence Cl A = the carrier of X by TDLAT_3:19; ::_thesis: verum end; end; theorem Th10: :: TEX_1:10 for X being non empty anti-discrete TopSpace for A being Subset of X holds ( ( A <> the carrier of X implies Int A = {} ) & ( A = the carrier of X implies Int A = the carrier of X ) ) proof let X be non empty anti-discrete TopSpace; ::_thesis: for A being Subset of X holds ( ( A <> the carrier of X implies Int A = {} ) & ( A = the carrier of X implies Int A = the carrier of X ) ) let A be Subset of X; ::_thesis: ( ( A <> the carrier of X implies Int A = {} ) & ( A = the carrier of X implies Int A = the carrier of X ) ) thus ( A <> the carrier of X implies Int A = {} ) ::_thesis: ( A = the carrier of X implies Int A = the carrier of X ) proof assume A1: A <> the carrier of X ; ::_thesis: Int A = {} now__::_thesis:_not_Int_A_=_the_carrier_of_X assume Int A = the carrier of X ; ::_thesis: contradiction then the carrier of X c= A by TOPS_1:16; hence contradiction by A1, XBOOLE_0:def_10; ::_thesis: verum end; hence Int A = {} by TDLAT_3:18; ::_thesis: verum end; thus ( A = the carrier of X implies Int A = the carrier of X ) ::_thesis: verum proof assume A = the carrier of X ; ::_thesis: Int A = the carrier of X then A = [#] X ; hence Int A = the carrier of X by TOPS_1:15; ::_thesis: verum end; end; theorem Th11: :: TEX_1:11 for X being non empty TopSpace st ( for A being Subset of X st not A is empty holds Cl A = the carrier of X ) holds X is anti-discrete proof let X be non empty TopSpace; ::_thesis: ( ( for A being Subset of X st not A is empty holds Cl A = the carrier of X ) implies X is anti-discrete ) assume A1: for A being Subset of X st not A is empty holds Cl A = the carrier of X ; ::_thesis: X is anti-discrete now__::_thesis:_for_A_being_Subset_of_X_holds_ (_not_A_is_closed_or_A_=_{}_or_A_=_the_carrier_of_X_) let A be Subset of X; ::_thesis: ( not A is closed or A = {} or A = the carrier of X ) assume A is closed ; ::_thesis: ( A = {} or A = the carrier of X ) then A = Cl A by PRE_TOPC:22; hence ( A = {} or A = the carrier of X ) by A1; ::_thesis: verum end; hence X is anti-discrete by TDLAT_3:19; ::_thesis: verum end; theorem Th12: :: TEX_1:12 for X being non empty TopSpace st ( for A being Subset of X st A <> the carrier of X holds Int A = {} ) holds X is anti-discrete proof let X be non empty TopSpace; ::_thesis: ( ( for A being Subset of X st A <> the carrier of X holds Int A = {} ) implies X is anti-discrete ) assume A1: for A being Subset of X st A <> the carrier of X holds Int A = {} ; ::_thesis: X is anti-discrete now__::_thesis:_for_A_being_Subset_of_X_holds_ (_not_A_is_open_or_A_=_{}_or_A_=_the_carrier_of_X_) let A be Subset of X; ::_thesis: ( not A is open or A = {} or A = the carrier of X ) assume A is open ; ::_thesis: ( A = {} or A = the carrier of X ) then A = Int A by TOPS_1:23; hence ( A = {} or A = the carrier of X ) by A1; ::_thesis: verum end; hence X is anti-discrete by TDLAT_3:18; ::_thesis: verum end; theorem :: TEX_1:13 for X being non empty anti-discrete TopSpace for A being Subset of X holds ( ( A <> {} implies A is dense ) & ( A <> the carrier of X implies A is boundary ) ) proof let X be non empty anti-discrete TopSpace; ::_thesis: for A being Subset of X holds ( ( A <> {} implies A is dense ) & ( A <> the carrier of X implies A is boundary ) ) let A be Subset of X; ::_thesis: ( ( A <> {} implies A is dense ) & ( A <> the carrier of X implies A is boundary ) ) thus ( A <> {} implies A is dense ) ::_thesis: ( A <> the carrier of X implies A is boundary ) proof assume A <> {} ; ::_thesis: A is dense then Cl A = the carrier of X by Th9; hence A is dense by TOPS_3:def_2; ::_thesis: verum end; thus ( A <> the carrier of X implies A is boundary ) ::_thesis: verum proof assume A <> the carrier of X ; ::_thesis: A is boundary then Int A = {} by Th10; hence A is boundary by TOPS_1:48; ::_thesis: verum end; end; theorem :: TEX_1:14 for X being non empty TopSpace st ( for A being Subset of X st A <> {} holds A is dense ) holds X is anti-discrete proof let X be non empty TopSpace; ::_thesis: ( ( for A being Subset of X st A <> {} holds A is dense ) implies X is anti-discrete ) assume A1: for A being Subset of X st A <> {} holds A is dense ; ::_thesis: X is anti-discrete now__::_thesis:_for_A_being_Subset_of_X_st_not_A_is_empty_holds_ Cl_A_=_the_carrier_of_X let A be Subset of X; ::_thesis: ( not A is empty implies Cl A = the carrier of X ) reconsider B = A as Subset of X ; assume not A is empty ; ::_thesis: Cl A = the carrier of X then B is dense by A1; hence Cl A = the carrier of X by TOPS_3:def_2; ::_thesis: verum end; hence X is anti-discrete by Th11; ::_thesis: verum end; theorem :: TEX_1:15 for X being non empty TopSpace st ( for A being Subset of X st A <> the carrier of X holds A is boundary ) holds X is anti-discrete proof let X be non empty TopSpace; ::_thesis: ( ( for A being Subset of X st A <> the carrier of X holds A is boundary ) implies X is anti-discrete ) assume A1: for A being Subset of X st A <> the carrier of X holds A is boundary ; ::_thesis: X is anti-discrete now__::_thesis:_for_A_being_Subset_of_X_st_A_<>_the_carrier_of_X_holds_ Int_A_=_{} let A be Subset of X; ::_thesis: ( A <> the carrier of X implies Int A = {} ) reconsider B = A as Subset of X ; assume A <> the carrier of X ; ::_thesis: Int A = {} then B is boundary by A1; hence Int A = {} ; ::_thesis: verum end; hence X is anti-discrete by Th12; ::_thesis: verum end; registration let D be set ; cluster 1TopSp D -> discrete ; coherence 1TopSp D is discrete by TDLAT_3:def_1; end; theorem :: TEX_1:16 for X being non empty discrete TopSpace for A being Subset of X holds ( Cl A = A & Int A = A ) proof let X be non empty discrete TopSpace; ::_thesis: for A being Subset of X holds ( Cl A = A & Int A = A ) let A be Subset of X; ::_thesis: ( Cl A = A & Int A = A ) reconsider B = A as Subset of X ; A1: B is closed by TDLAT_3:16; B is open by TDLAT_3:15; hence ( Cl A = A & Int A = A ) by A1, PRE_TOPC:22, TOPS_1:23; ::_thesis: verum end; theorem :: TEX_1:17 for X being non empty TopSpace st ( for A being Subset of X holds Cl A = A ) holds X is discrete proof let X be non empty TopSpace; ::_thesis: ( ( for A being Subset of X holds Cl A = A ) implies X is discrete ) assume A1: for A being Subset of X holds Cl A = A ; ::_thesis: X is discrete now__::_thesis:_for_A_being_Subset_of_X_holds_A_is_closed let A be Subset of X; ::_thesis: A is closed Cl A = A by A1; hence A is closed ; ::_thesis: verum end; hence X is discrete by TDLAT_3:16; ::_thesis: verum end; theorem :: TEX_1:18 for X being non empty TopSpace st ( for A being Subset of X holds Int A = A ) holds X is discrete proof let X be non empty TopSpace; ::_thesis: ( ( for A being Subset of X holds Int A = A ) implies X is discrete ) assume A1: for A being Subset of X holds Int A = A ; ::_thesis: X is discrete now__::_thesis:_for_A_being_Subset_of_X_holds_A_is_open let A be Subset of X; ::_thesis: A is open Int A = A by A1; hence A is open ; ::_thesis: verum end; hence X is discrete by TDLAT_3:15; ::_thesis: verum end; theorem Th19: :: TEX_1:19 for D being non empty set holds ( ADTS D = 1TopSp D iff ex d0 being Element of D st D = {d0} ) proof let D be non empty set ; ::_thesis: ( ADTS D = 1TopSp D iff ex d0 being Element of D st D = {d0} ) thus ( ADTS D = 1TopSp D implies ex d0 being Element of D st D = {d0} ) ::_thesis: ( ex d0 being Element of D st D = {d0} implies ADTS D = 1TopSp D ) proof set d0 = the Element of D; assume A1: ADTS D = 1TopSp D ; ::_thesis: ex d0 being Element of D st D = {d0} take the Element of D ; ::_thesis: D = { the Element of D} thus D = { the Element of D} by A1, TARSKI:def_2; ::_thesis: verum end; given d0 being Element of D such that A2: D = {d0} ; ::_thesis: ADTS D = 1TopSp D thus ADTS D = 1TopSp D by A2, ZFMISC_1:24; ::_thesis: verum end; registration cluster non empty strict TopSpace-like discrete non anti-discrete for TopStruct ; existence ex b1 being TopSpace st ( b1 is discrete & not b1 is anti-discrete & b1 is strict & not b1 is empty ) proof set D = {{},1}; set Y = 1TopSp {{},1}; take 1TopSp {{},1} ; ::_thesis: ( 1TopSp {{},1} is discrete & not 1TopSp {{},1} is anti-discrete & 1TopSp {{},1} is strict & not 1TopSp {{},1} is empty ) now__::_thesis:_not_1TopSp_{{},1}_is_anti-discrete assume 1TopSp {{},1} is anti-discrete ; ::_thesis: contradiction then TopStruct(# the carrier of (1TopSp {{},1}), the topology of (1TopSp {{},1}) #) = TopStruct(# the carrier of (ADTS {{},1}), the topology of (ADTS {{},1}) #) by TDLAT_3:def_2; then consider d0 being Element of {{},1} such that A1: {{},1} = {d0} by Th19; d0 = {} by A1, ZFMISC_1:4; hence contradiction by A1, ZFMISC_1:4; ::_thesis: verum end; hence ( 1TopSp {{},1} is discrete & not 1TopSp {{},1} is anti-discrete & 1TopSp {{},1} is strict & not 1TopSp {{},1} is empty ) ; ::_thesis: verum end; cluster non empty strict TopSpace-like non discrete anti-discrete for TopStruct ; existence ex b1 being TopSpace st ( b1 is anti-discrete & not b1 is discrete & b1 is strict & not b1 is empty ) proof set D = {{},1}; set Y = ADTS {{},1}; take ADTS {{},1} ; ::_thesis: ( ADTS {{},1} is anti-discrete & not ADTS {{},1} is discrete & ADTS {{},1} is strict & not ADTS {{},1} is empty ) now__::_thesis:_not_ADTS_{{},1}_is_discrete assume ADTS {{},1} is discrete ; ::_thesis: contradiction then TopStruct(# the carrier of (ADTS {{},1}), the topology of (ADTS {{},1}) #) = TopStruct(# the carrier of (1TopSp {{},1}), the topology of (1TopSp {{},1}) #) by TDLAT_3:def_1; then consider d0 being Element of {{},1} such that A2: {{},1} = {d0} by Th19; d0 = {} by A2, ZFMISC_1:4; hence contradiction by A2, ZFMISC_1:4; ::_thesis: verum end; hence ( ADTS {{},1} is anti-discrete & not ADTS {{},1} is discrete & ADTS {{},1} is strict & not ADTS {{},1} is empty ) ; ::_thesis: verum end; end; begin definition let D be set ; let d0 be Element of D; func STS (D,d0) -> TopStruct equals :: TEX_1:def 4 TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #); coherence TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) is TopStruct ; end; :: deftheorem defines STS TEX_1:def_4_:_ for D being set for d0 being Element of D holds STS (D,d0) = TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #); registration let D be set ; let d0 be Element of D; cluster STS (D,d0) -> strict TopSpace-like ; coherence ( STS (D,d0) is strict & STS (D,d0) is TopSpace-like ) proof reconsider E = D as Subset of D by Lm1; set G = { A where A is Subset of D : ( d0 in A & A <> D ) } ; set T = (bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ; set Y = TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #); thus STS (D,d0) is strict ; ::_thesis: STS (D,d0) is TopSpace-like for A being Subset of D holds ( not A = E or not d0 in A or not A <> D ) ; then A1: not E in { A where A is Subset of D : ( d0 in A & A <> D ) } ; A2: now__::_thesis:_for_F_being_Subset-Family_of_TopStruct(#_D,((bool_D)_\__{__A_where_A_is_Subset_of_D_:_(_d0_in_A_&_A_<>_D_)__}__)_#)_st_F_c=_the_topology_of_TopStruct(#_D,((bool_D)_\__{__A_where_A_is_Subset_of_D_:_(_d0_in_A_&_A_<>_D_)__}__)_#)_holds_ union_F_in_the_topology_of_TopStruct(#_D,((bool_D)_\__{__A_where_A_is_Subset_of_D_:_(_d0_in_A_&_A_<>_D_)__}__)_#) let F be Subset-Family of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #); ::_thesis: ( F c= the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) implies union F in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) ) assume F c= the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) ; ::_thesis: union F in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) then F misses { A where A is Subset of D : ( d0 in A & A <> D ) } by XBOOLE_1:63, XBOOLE_1:79; then A3: F /\ { A where A is Subset of D : ( d0 in A & A <> D ) } = {} by XBOOLE_0:def_7; now__::_thesis:_(_(_union_F_=_D_&_union_F_in_the_topology_of_TopStruct(#_D,((bool_D)_\__{__A_where_A_is_Subset_of_D_:_(_d0_in_A_&_A_<>_D_)__}__)_#)_)_or_(_union_F_<>_D_&_union_F_in_the_topology_of_TopStruct(#_D,((bool_D)_\__{__A_where_A_is_Subset_of_D_:_(_d0_in_A_&_A_<>_D_)__}__)_#)_)_) percases ( union F = D or union F <> D ) ; case union F = D ; ::_thesis: union F in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) hence union F in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) by A1, XBOOLE_0:def_5; ::_thesis: verum end; caseA4: union F <> D ; ::_thesis: union F in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) A5: now__::_thesis:_for_A_being_Subset_of_D_st_A_in_F_holds_ not_A_=_D let A be Subset of D; ::_thesis: ( A in F implies not A = D ) assume A6: A in F ; ::_thesis: not A = D assume A = D ; ::_thesis: contradiction then D c= union F by A6, ZFMISC_1:74; hence contradiction by A4, XBOOLE_0:def_10; ::_thesis: verum end; now__::_thesis:_for_A_being_set_st_A_in_F_holds_ not_d0_in_A let A be set ; ::_thesis: ( A in F implies not d0 in A ) assume A7: A in F ; ::_thesis: not d0 in A then reconsider B = A as Subset of D ; not B in { A where A is Subset of D : ( d0 in A & A <> D ) } by A3, A7, XBOOLE_0:def_4; then ( not d0 in B or not B <> D ) ; hence not d0 in A by A5, A7; ::_thesis: verum end; then for A being set holds ( not d0 in A or not A in F ) ; then for A being Subset of D holds ( not A = union F or not d0 in A or not A <> D ) by TARSKI:def_4; then not union F in { A where A is Subset of D : ( d0 in A & A <> D ) } ; hence union F in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) by XBOOLE_0:def_5; ::_thesis: verum end; end; end; hence union F in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) ; ::_thesis: verum end; A8: now__::_thesis:_for_C,_E_being_Subset_of_TopStruct(#_D,((bool_D)_\__{__A_where_A_is_Subset_of_D_:_(_d0_in_A_&_A_<>_D_)__}__)_#)_st_C_in_the_topology_of_TopStruct(#_D,((bool_D)_\__{__A_where_A_is_Subset_of_D_:_(_d0_in_A_&_A_<>_D_)__}__)_#)_&_E_in_the_topology_of_TopStruct(#_D,((bool_D)_\__{__A_where_A_is_Subset_of_D_:_(_d0_in_A_&_A_<>_D_)__}__)_#)_holds_ C_/\_E_in_the_topology_of_TopStruct(#_D,((bool_D)_\__{__A_where_A_is_Subset_of_D_:_(_d0_in_A_&_A_<>_D_)__}__)_#) let C, E be Subset of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #); ::_thesis: ( C in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) & E in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) implies C /\ E in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) ) assume that A9: C in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) and A10: E in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) ; ::_thesis: C /\ E in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) A11: now__::_thesis:_for_P_being_Subset_of_D_st_P_in_the_topology_of_TopStruct(#_D,((bool_D)_\__{__A_where_A_is_Subset_of_D_:_(_d0_in_A_&_A_<>_D_)__}__)_#)_&_P_<>_D_holds_ not_d0_in_P let P be Subset of D; ::_thesis: ( P in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) & P <> D implies not d0 in P ) assume that A12: P in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) and A13: P <> D ; ::_thesis: not d0 in P not P in { A where A is Subset of D : ( d0 in A & A <> D ) } by A12, XBOOLE_0:def_5; hence not d0 in P by A13; ::_thesis: verum end; now__::_thesis:_(_(_C_=_D_&_E_=_D_&_C_/\_E_in_the_topology_of_TopStruct(#_D,((bool_D)_\__{__A_where_A_is_Subset_of_D_:_(_d0_in_A_&_A_<>_D_)__}__)_#)_)_or_(_(_C_<>_D_or_E_<>_D_)_&_C_/\_E_in_the_topology_of_TopStruct(#_D,((bool_D)_\__{__A_where_A_is_Subset_of_D_:_(_d0_in_A_&_A_<>_D_)__}__)_#)_)_) percases ( ( C = D & E = D ) or C <> D or E <> D ) ; case ( C = D & E = D ) ; ::_thesis: C /\ E in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) hence C /\ E in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) by A1, XBOOLE_0:def_5; ::_thesis: verum end; caseA14: ( C <> D or E <> D ) ; ::_thesis: C /\ E in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) now__::_thesis:_(_(_C_<>_D_&_C_/\_E_in_the_topology_of_TopStruct(#_D,((bool_D)_\__{__A_where_A_is_Subset_of_D_:_(_d0_in_A_&_A_<>_D_)__}__)_#)_)_or_(_E_<>_D_&_C_/\_E_in_the_topology_of_TopStruct(#_D,((bool_D)_\__{__A_where_A_is_Subset_of_D_:_(_d0_in_A_&_A_<>_D_)__}__)_#)_)_) percases ( C <> D or E <> D ) by A14; caseA15: C <> D ; ::_thesis: C /\ E in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) C /\ E c= C by XBOOLE_1:17; then for A being Subset of D holds ( not A = C /\ E or not d0 in A or not A <> D ) by A9, A11, A15; then not C /\ E in { A where A is Subset of D : ( d0 in A & A <> D ) } ; hence C /\ E in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) by XBOOLE_0:def_5; ::_thesis: verum end; caseA16: E <> D ; ::_thesis: C /\ E in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) C /\ E c= E by XBOOLE_1:17; then for A being Subset of D holds ( not A = C /\ E or not d0 in A or not A <> D ) by A10, A11, A16; then not C /\ E in { A where A is Subset of D : ( d0 in A & A <> D ) } ; hence C /\ E in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) by XBOOLE_0:def_5; ::_thesis: verum end; end; end; hence C /\ E in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) ; ::_thesis: verum end; end; end; hence C /\ E in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) ; ::_thesis: verum end; the carrier of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) in the topology of TopStruct(# D,((bool D) \ { A where A is Subset of D : ( d0 in A & A <> D ) } ) #) by A1, XBOOLE_0:def_5; hence STS (D,d0) is TopSpace-like by A2, A8, PRE_TOPC:def_1; ::_thesis: verum end; end; registration let D be non empty set ; let d0 be Element of D; cluster STS (D,d0) -> non empty ; coherence not STS (D,d0) is empty ; end; theorem Th20: :: TEX_1:20 for D being non empty set for d0 being Element of D for A being Subset of (STS (D,d0)) holds ( ( {d0} c= A implies A is closed ) & ( not A is empty & A is closed implies {d0} c= A ) ) proof let D be non empty set ; ::_thesis: for d0 being Element of D for A being Subset of (STS (D,d0)) holds ( ( {d0} c= A implies A is closed ) & ( not A is empty & A is closed implies {d0} c= A ) ) let d0 be Element of D; ::_thesis: for A being Subset of (STS (D,d0)) holds ( ( {d0} c= A implies A is closed ) & ( not A is empty & A is closed implies {d0} c= A ) ) let A be Subset of (STS (D,d0)); ::_thesis: ( ( {d0} c= A implies A is closed ) & ( not A is empty & A is closed implies {d0} c= A ) ) set Z = A ` ; set G = { P where P is Subset of D : ( d0 in P & P <> D ) } ; thus ( {d0} c= A implies A is closed ) ::_thesis: ( not A is empty & A is closed implies {d0} c= A ) proof A1: d0 in {d0} by TARSKI:def_1; assume {d0} c= A ; ::_thesis: A is closed then for Q being Subset of D holds ( not Q = A ` or not d0 in Q or not Q <> D ) by A1, XBOOLE_0:def_5; then not A ` in { P where P is Subset of D : ( d0 in P & P <> D ) } ; then A ` in the topology of (STS (D,d0)) by XBOOLE_0:def_5; then A ` is open by PRE_TOPC:def_2; hence A is closed by TOPS_1:3; ::_thesis: verum end; assume not A is empty ; ::_thesis: ( not A is closed or {d0} c= A ) then A2: A ` <> D by TOPS_3:1; assume A is closed ; ::_thesis: {d0} c= A then A ` in the topology of (STS (D,d0)) by PRE_TOPC:def_2; then not A ` in { P where P is Subset of D : ( d0 in P & P <> D ) } by XBOOLE_0:def_5; then not d0 in A ` by A2; then d0 in A by SUBSET_1:29; hence {d0} c= A by ZFMISC_1:31; ::_thesis: verum end; theorem Th21: :: TEX_1:21 for D being non empty set for d0 being Element of D st not D \ {d0} is empty holds for A being Subset of (STS (D,d0)) holds ( ( A = {d0} implies ( A is closed & A is boundary ) ) & ( not A is empty & A is closed & A is boundary implies A = {d0} ) ) proof let D be non empty set ; ::_thesis: for d0 being Element of D st not D \ {d0} is empty holds for A being Subset of (STS (D,d0)) holds ( ( A = {d0} implies ( A is closed & A is boundary ) ) & ( not A is empty & A is closed & A is boundary implies A = {d0} ) ) let d0 be Element of D; ::_thesis: ( not D \ {d0} is empty implies for A being Subset of (STS (D,d0)) holds ( ( A = {d0} implies ( A is closed & A is boundary ) ) & ( not A is empty & A is closed & A is boundary implies A = {d0} ) ) ) assume A1: not D \ {d0} is empty ; ::_thesis: for A being Subset of (STS (D,d0)) holds ( ( A = {d0} implies ( A is closed & A is boundary ) ) & ( not A is empty & A is closed & A is boundary implies A = {d0} ) ) set G = { P where P is Subset of D : ( d0 in P & P <> D ) } ; let A be Subset of (STS (D,d0)); ::_thesis: ( ( A = {d0} implies ( A is closed & A is boundary ) ) & ( not A is empty & A is closed & A is boundary implies A = {d0} ) ) A2: Int A in the topology of (STS (D,d0)) by PRE_TOPC:def_2; thus ( A = {d0} implies ( A is closed & A is boundary ) ) ::_thesis: ( not A is empty & A is closed & A is boundary implies A = {d0} ) proof assume A3: A = {d0} ; ::_thesis: ( A is closed & A is boundary ) hence A is closed by Th20; ::_thesis: A is boundary A4: now__::_thesis:_not_Int_A_=_A assume A5: Int A = A ; ::_thesis: contradiction then A6: d0 in Int A by A3, TARSKI:def_1; Int A <> D by A1, A3, A5, XBOOLE_1:37; then Int A in { P where P is Subset of D : ( d0 in P & P <> D ) } by A6; hence contradiction by A2, XBOOLE_0:def_5; ::_thesis: verum end; Int A c= A by TOPS_1:16; then ( Int A = {} or Int A = A ) by A3, ZFMISC_1:33; hence A is boundary by A4, TOPS_1:48; ::_thesis: verum end; thus ( not A is empty & A is closed & A is boundary implies A = {d0} ) ::_thesis: verum proof set Z = A \ {d0}; assume that A7: not A is empty and A8: A is closed ; ::_thesis: ( not A is boundary or A = {d0} ) A9: {d0} c= A by A7, A8, Th20; A10: A \ {d0} c= A by XBOOLE_1:36; reconsider Z = A \ {d0} as Subset of (STS (D,d0)) ; d0 in {d0} by TARSKI:def_1; then for Q being Subset of D holds ( not Q = Z or not d0 in Q or not Q <> D ) by XBOOLE_0:def_5; then not Z in { P where P is Subset of D : ( d0 in P & P <> D ) } ; then Z in the topology of (STS (D,d0)) by XBOOLE_0:def_5; then A11: Z is open by PRE_TOPC:def_2; assume A is boundary ; ::_thesis: A = {d0} then A12: Int A = {} ; assume A13: A <> {d0} ; ::_thesis: contradiction now__::_thesis:_not_Z_=_{} assume Z = {} ; ::_thesis: contradiction then A c= {d0} by XBOOLE_1:37; hence contradiction by A9, A13, XBOOLE_0:def_10; ::_thesis: verum end; hence contradiction by A10, A12, A11, TOPS_1:24, XBOOLE_1:3; ::_thesis: verum end; end; theorem Th22: :: TEX_1:22 for D being non empty set for d0 being Element of D for A being Subset of (STS (D,d0)) holds ( ( A c= D \ {d0} implies A is open ) & ( A <> D & A is open implies A c= D \ {d0} ) ) proof let D be non empty set ; ::_thesis: for d0 being Element of D for A being Subset of (STS (D,d0)) holds ( ( A c= D \ {d0} implies A is open ) & ( A <> D & A is open implies A c= D \ {d0} ) ) let d0 be Element of D; ::_thesis: for A being Subset of (STS (D,d0)) holds ( ( A c= D \ {d0} implies A is open ) & ( A <> D & A is open implies A c= D \ {d0} ) ) let A be Subset of (STS (D,d0)); ::_thesis: ( ( A c= D \ {d0} implies A is open ) & ( A <> D & A is open implies A c= D \ {d0} ) ) set Z = A ` ; reconsider P = {d0} as Subset of (STS (D,d0)) ; thus ( A c= D \ {d0} implies A is open ) ::_thesis: ( A <> D & A is open implies A c= D \ {d0} ) proof assume A c= D \ {d0} ; ::_thesis: A is open then ([#] (STS (D,d0))) \ (D \ {d0}) c= ([#] (STS (D,d0))) \ A by XBOOLE_1:34; then P c= A ` by PRE_TOPC:3; then A ` is closed by Th20; hence A is open by TOPS_1:4; ::_thesis: verum end; thus ( A <> D & A is open implies A c= D \ {d0} ) ::_thesis: verum proof assume A <> D ; ::_thesis: ( not A is open or A c= D \ {d0} ) then A1: A ` <> {} (STS (D,d0)) by TOPS_3:2; assume A is open ; ::_thesis: A c= D \ {d0} then {d0} c= A ` by A1, Th20; then (A `) ` c= P ` by SUBSET_1:12; hence A c= D \ {d0} ; ::_thesis: verum end; end; theorem :: TEX_1:23 for D being non empty set for d0 being Element of D st not D \ {d0} is empty holds for A being Subset of (STS (D,d0)) holds ( ( A = D \ {d0} implies ( A is open & A is dense ) ) & ( A <> D & A is open & A is dense implies A = D \ {d0} ) ) proof let D be non empty set ; ::_thesis: for d0 being Element of D st not D \ {d0} is empty holds for A being Subset of (STS (D,d0)) holds ( ( A = D \ {d0} implies ( A is open & A is dense ) ) & ( A <> D & A is open & A is dense implies A = D \ {d0} ) ) let d0 be Element of D; ::_thesis: ( not D \ {d0} is empty implies for A being Subset of (STS (D,d0)) holds ( ( A = D \ {d0} implies ( A is open & A is dense ) ) & ( A <> D & A is open & A is dense implies A = D \ {d0} ) ) ) assume A1: not D \ {d0} is empty ; ::_thesis: for A being Subset of (STS (D,d0)) holds ( ( A = D \ {d0} implies ( A is open & A is dense ) ) & ( A <> D & A is open & A is dense implies A = D \ {d0} ) ) reconsider P = {d0} as Subset of (STS (D,d0)) ; let A be Subset of (STS (D,d0)); ::_thesis: ( ( A = D \ {d0} implies ( A is open & A is dense ) ) & ( A <> D & A is open & A is dense implies A = D \ {d0} ) ) set Z = A ` ; thus ( A = D \ {d0} implies ( A is open & A is dense ) ) ::_thesis: ( A <> D & A is open & A is dense implies A = D \ {d0} ) proof assume A2: A = D \ {d0} ; ::_thesis: ( A is open & A is dense ) hence A is open by Th22; ::_thesis: A is dense ([#] (STS (D,d0))) \ (([#] (STS (D,d0))) \ P) = A ` by A2; then P = A ` by PRE_TOPC:3; then A ` is boundary by A1, Th21; hence A is dense by TOPS_3:18; ::_thesis: verum end; thus ( A <> D & A is open & A is dense implies A = D \ {d0} ) ::_thesis: verum proof assume A <> D ; ::_thesis: ( not A is open or not A is dense or A = D \ {d0} ) then A3: A ` <> {} (STS (D,d0)) by TOPS_3:2; assume A4: A is open ; ::_thesis: ( not A is dense or A = D \ {d0} ) assume A is dense ; ::_thesis: A = D \ {d0} then A ` is boundary by TOPS_3:18; then A ` = {d0} by A1, A3, A4, Th21; then A = P ` ; hence A = D \ {d0} ; ::_thesis: verum end; end; registration cluster non empty strict TopSpace-like non discrete non anti-discrete for TopStruct ; existence ex b1 being TopSpace st ( not b1 is anti-discrete & not b1 is discrete & b1 is strict & not b1 is empty ) proof set D = {{},1}; reconsider a = {} as Element of {{},1} by TARSKI:def_2; set Y = STS ({{},1},a); take STS ({{},1},a) ; ::_thesis: ( not STS ({{},1},a) is anti-discrete & not STS ({{},1},a) is discrete & STS ({{},1},a) is strict & not STS ({{},1},a) is empty ) reconsider A = {a} as non empty Subset of (STS ({{},1},a)) ; A1: not 1 in A by TARSKI:def_1; A2: 1 in {{},1} by TARSKI:def_2; then A3: not {{},1} \ A is empty by A1, XBOOLE_0:def_5; then A is boundary by Th21; then Int A <> A ; then A4: not A is open by TOPS_1:23; A is closed by A3, Th21; hence ( not STS ({{},1},a) is anti-discrete & not STS ({{},1},a) is discrete & STS ({{},1},a) is strict & not STS ({{},1},a) is empty ) by A2, A1, A4, TDLAT_3:15, TDLAT_3:19; ::_thesis: verum end; end; theorem Th24: :: TEX_1:24 for D being non empty set for d0 being Element of D for Y being non empty TopSpace holds ( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) iff ( the carrier of Y = D & ( for A being Subset of Y holds ( ( {d0} c= A implies A is closed ) & ( not A is empty & A is closed implies {d0} c= A ) ) ) ) ) proof let D be non empty set ; ::_thesis: for d0 being Element of D for Y being non empty TopSpace holds ( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) iff ( the carrier of Y = D & ( for A being Subset of Y holds ( ( {d0} c= A implies A is closed ) & ( not A is empty & A is closed implies {d0} c= A ) ) ) ) ) let d0 be Element of D; ::_thesis: for Y being non empty TopSpace holds ( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) iff ( the carrier of Y = D & ( for A being Subset of Y holds ( ( {d0} c= A implies A is closed ) & ( not A is empty & A is closed implies {d0} c= A ) ) ) ) ) let Y be non empty TopSpace; ::_thesis: ( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) iff ( the carrier of Y = D & ( for A being Subset of Y holds ( ( {d0} c= A implies A is closed ) & ( not A is empty & A is closed implies {d0} c= A ) ) ) ) ) thus ( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) implies ( the carrier of Y = D & ( for A being Subset of Y holds ( ( {d0} c= A implies A is closed ) & ( not A is empty & A is closed implies {d0} c= A ) ) ) ) ) ::_thesis: ( the carrier of Y = D & ( for A being Subset of Y holds ( ( {d0} c= A implies A is closed ) & ( not A is empty & A is closed implies {d0} c= A ) ) ) implies TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) ) proof assume A1: TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) ; ::_thesis: ( the carrier of Y = D & ( for A being Subset of Y holds ( ( {d0} c= A implies A is closed ) & ( not A is empty & A is closed implies {d0} c= A ) ) ) ) hence the carrier of Y = D ; ::_thesis: for A being Subset of Y holds ( ( {d0} c= A implies A is closed ) & ( not A is empty & A is closed implies {d0} c= A ) ) now__::_thesis:_for_A_being_Subset_of_Y_holds_ (_(_{d0}_c=_A_implies_A_is_closed_)_&_(_not_A_is_empty_&_A_is_closed_implies_{d0}_c=_A_)_) let A be Subset of Y; ::_thesis: ( ( {d0} c= A implies A is closed ) & ( not A is empty & A is closed implies {d0} c= A ) ) reconsider B = A as Subset of (STS (D,d0)) by A1; thus ( {d0} c= A implies A is closed ) ::_thesis: ( not A is empty & A is closed implies {d0} c= A ) proof assume {d0} c= A ; ::_thesis: A is closed then B is closed by Th20; hence A is closed by A1, TOPS_3:79; ::_thesis: verum end; thus ( not A is empty & A is closed implies {d0} c= A ) ::_thesis: verum proof assume A2: not A is empty ; ::_thesis: ( not A is closed or {d0} c= A ) assume A is closed ; ::_thesis: {d0} c= A then B is closed by A1, TOPS_3:79; hence {d0} c= A by A2, Th20; ::_thesis: verum end; end; hence for A being Subset of Y holds ( ( {d0} c= A implies A is closed ) & ( not A is empty & A is closed implies {d0} c= A ) ) ; ::_thesis: verum end; assume A3: the carrier of Y = D ; ::_thesis: ( ex A being Subset of Y st ( ( {d0} c= A implies A is closed ) implies ( not A is empty & A is closed & not {d0} c= A ) ) or TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) ) assume A4: for A being Subset of Y holds ( ( {d0} c= A implies A is closed ) & ( not A is empty & A is closed implies {d0} c= A ) ) ; ::_thesis: TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) now__::_thesis:_for_A_being_Subset_of_Y for_C_being_Subset_of_(STS_(D,d0))_st_A_=_C_holds_ (_A_is_closed_iff_C_is_closed_) let A be Subset of Y; ::_thesis: for C being Subset of (STS (D,d0)) st A = C holds ( A is closed iff C is closed ) let C be Subset of (STS (D,d0)); ::_thesis: ( A = C implies ( A is closed iff C is closed ) ) assume A5: A = C ; ::_thesis: ( A is closed iff C is closed ) A6: now__::_thesis:_(_C_is_closed_implies_A_is_closed_) assume A7: C is closed ; ::_thesis: A is closed now__::_thesis:_(_(_C_=_{}_&_A_is_closed_)_or_(_C_<>_{}_&_A_is_closed_)_) percases ( C = {} or C <> {} ) ; case C = {} ; ::_thesis: A is closed hence A is closed by A5; ::_thesis: verum end; case C <> {} ; ::_thesis: A is closed then {d0} c= A by A5, A7, Th20; hence A is closed by A4; ::_thesis: verum end; end; end; hence A is closed ; ::_thesis: verum end; now__::_thesis:_(_A_is_closed_implies_C_is_closed_) assume A8: A is closed ; ::_thesis: C is closed now__::_thesis:_(_(_A_=_{}_&_C_is_closed_)_or_(_A_<>_{}_&_C_is_closed_)_) percases ( A = {} or A <> {} ) ; case A = {} ; ::_thesis: C is closed hence C is closed by A5; ::_thesis: verum end; case A <> {} ; ::_thesis: C is closed then {d0} c= C by A4, A5, A8; hence C is closed by Th20; ::_thesis: verum end; end; end; hence C is closed ; ::_thesis: verum end; hence ( A is closed iff C is closed ) by A6; ::_thesis: verum end; hence TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) by A3, TOPS_3:73; ::_thesis: verum end; theorem Th25: :: TEX_1:25 for D being non empty set for d0 being Element of D for Y being non empty TopSpace holds ( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) iff ( the carrier of Y = D & ( for A being Subset of Y holds ( ( A c= D \ {d0} implies A is open ) & ( A <> D & A is open implies A c= D \ {d0} ) ) ) ) ) proof let D be non empty set ; ::_thesis: for d0 being Element of D for Y being non empty TopSpace holds ( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) iff ( the carrier of Y = D & ( for A being Subset of Y holds ( ( A c= D \ {d0} implies A is open ) & ( A <> D & A is open implies A c= D \ {d0} ) ) ) ) ) let d0 be Element of D; ::_thesis: for Y being non empty TopSpace holds ( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) iff ( the carrier of Y = D & ( for A being Subset of Y holds ( ( A c= D \ {d0} implies A is open ) & ( A <> D & A is open implies A c= D \ {d0} ) ) ) ) ) let Y be non empty TopSpace; ::_thesis: ( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) iff ( the carrier of Y = D & ( for A being Subset of Y holds ( ( A c= D \ {d0} implies A is open ) & ( A <> D & A is open implies A c= D \ {d0} ) ) ) ) ) thus ( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) implies ( the carrier of Y = D & ( for A being Subset of Y holds ( ( A c= D \ {d0} implies A is open ) & ( A <> D & A is open implies A c= D \ {d0} ) ) ) ) ) ::_thesis: ( the carrier of Y = D & ( for A being Subset of Y holds ( ( A c= D \ {d0} implies A is open ) & ( A <> D & A is open implies A c= D \ {d0} ) ) ) implies TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) ) proof assume A1: TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) ; ::_thesis: ( the carrier of Y = D & ( for A being Subset of Y holds ( ( A c= D \ {d0} implies A is open ) & ( A <> D & A is open implies A c= D \ {d0} ) ) ) ) hence the carrier of Y = D ; ::_thesis: for A being Subset of Y holds ( ( A c= D \ {d0} implies A is open ) & ( A <> D & A is open implies A c= D \ {d0} ) ) let A be Subset of Y; ::_thesis: ( ( A c= D \ {d0} implies A is open ) & ( A <> D & A is open implies A c= D \ {d0} ) ) reconsider B = A as Subset of (STS (D,d0)) by A1; thus ( A c= D \ {d0} implies A is open ) ::_thesis: ( A <> D & A is open implies A c= D \ {d0} ) proof assume A c= D \ {d0} ; ::_thesis: A is open then B is open by Th22; hence A is open by A1, TOPS_3:76; ::_thesis: verum end; thus ( A <> D & A is open implies A c= D \ {d0} ) ::_thesis: verum proof assume A2: A <> D ; ::_thesis: ( not A is open or A c= D \ {d0} ) assume A is open ; ::_thesis: A c= D \ {d0} then B is open by A1, TOPS_3:76; hence A c= D \ {d0} by A2, Th22; ::_thesis: verum end; end; assume A3: the carrier of Y = D ; ::_thesis: ( ex A being Subset of Y st ( ( A c= D \ {d0} implies A is open ) implies ( A <> D & A is open & not A c= D \ {d0} ) ) or TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) ) assume A4: for A being Subset of Y holds ( ( A c= D \ {d0} implies A is open ) & ( A <> D & A is open implies A c= D \ {d0} ) ) ; ::_thesis: TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) now__::_thesis:_for_A_being_Subset_of_Y for_C_being_Subset_of_(STS_(D,d0))_st_A_=_C_holds_ (_A_is_open_iff_C_is_open_) let A be Subset of Y; ::_thesis: for C being Subset of (STS (D,d0)) st A = C holds ( A is open iff C is open ) let C be Subset of (STS (D,d0)); ::_thesis: ( A = C implies ( A is open iff C is open ) ) assume A5: A = C ; ::_thesis: ( A is open iff C is open ) A6: now__::_thesis:_(_A_is_open_implies_C_is_open_) assume A7: A is open ; ::_thesis: C is open now__::_thesis:_(_(_A_=_D_&_C_is_open_)_or_(_A_<>_D_&_C_is_open_)_) percases ( A = D or A <> D ) ; case A = D ; ::_thesis: C is open then C = [#] (STS (D,d0)) by A5; hence C is open ; ::_thesis: verum end; case A <> D ; ::_thesis: C is open then A c= D \ {d0} by A4, A7; hence C is open by A5, Th22; ::_thesis: verum end; end; end; hence C is open ; ::_thesis: verum end; now__::_thesis:_(_C_is_open_implies_A_is_open_) assume A8: C is open ; ::_thesis: A is open now__::_thesis:_(_(_C_=_D_&_A_is_open_)_or_(_C_<>_D_&_A_is_open_)_) percases ( C = D or C <> D ) ; case C = D ; ::_thesis: A is open then A = [#] Y by A3, A5; hence A is open ; ::_thesis: verum end; case C <> D ; ::_thesis: A is open then A c= D \ {d0} by A5, A8, Th22; hence A is open by A4; ::_thesis: verum end; end; end; hence A is open ; ::_thesis: verum end; hence ( A is open iff C is open ) by A6; ::_thesis: verum end; hence TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) by A3, TOPS_3:72; ::_thesis: verum end; theorem :: TEX_1:26 for D being non empty set for d0 being Element of D for Y being non empty TopSpace holds ( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) iff ( the carrier of Y = D & ( for A being non empty Subset of Y holds Cl A = A \/ {d0} ) ) ) proof let D be non empty set ; ::_thesis: for d0 being Element of D for Y being non empty TopSpace holds ( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) iff ( the carrier of Y = D & ( for A being non empty Subset of Y holds Cl A = A \/ {d0} ) ) ) let d0 be Element of D; ::_thesis: for Y being non empty TopSpace holds ( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) iff ( the carrier of Y = D & ( for A being non empty Subset of Y holds Cl A = A \/ {d0} ) ) ) let Y be non empty TopSpace; ::_thesis: ( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) iff ( the carrier of Y = D & ( for A being non empty Subset of Y holds Cl A = A \/ {d0} ) ) ) thus ( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) implies ( the carrier of Y = D & ( for A being non empty Subset of Y holds Cl A = A \/ {d0} ) ) ) ::_thesis: ( the carrier of Y = D & ( for A being non empty Subset of Y holds Cl A = A \/ {d0} ) implies TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) ) proof assume A1: TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) ; ::_thesis: ( the carrier of Y = D & ( for A being non empty Subset of Y holds Cl A = A \/ {d0} ) ) hence the carrier of Y = D ; ::_thesis: for A being non empty Subset of Y holds Cl A = A \/ {d0} reconsider P = {d0} as Subset of Y by A1; now__::_thesis:_for_A_being_non_empty_Subset_of_Y_holds_Cl_A_=_A_\/_{d0} let A be non empty Subset of Y; ::_thesis: Cl A = A \/ {d0} reconsider B = A as Subset of Y ; not Cl A is empty by PCOMPS_1:2; then A2: {d0} c= Cl A by A1, Th24; A c= Cl A by PRE_TOPC:18; then A3: A \/ {d0} c= Cl A by A2, XBOOLE_1:8; {d0} c= A \/ P by XBOOLE_1:7; then B \/ P is closed by A1, Th24; then A4: Cl (A \/ P) = A \/ {d0} by PRE_TOPC:22; Cl A c= Cl (A \/ P) by PRE_TOPC:19, XBOOLE_1:7; hence Cl A = A \/ {d0} by A4, A3, XBOOLE_0:def_10; ::_thesis: verum end; hence for A being non empty Subset of Y holds Cl A = A \/ {d0} ; ::_thesis: verum end; assume A5: the carrier of Y = D ; ::_thesis: ( ex A being non empty Subset of Y st not Cl A = A \/ {d0} or TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) ) assume A6: for A being non empty Subset of Y holds Cl A = A \/ {d0} ; ::_thesis: TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) now__::_thesis:_for_A_being_Subset_of_Y_holds_ (_(_{d0}_c=_A_implies_A_is_closed_)_&_(_not_A_is_empty_&_A_is_closed_implies_{d0}_c=_A_)_) let A be Subset of Y; ::_thesis: ( ( {d0} c= A implies A is closed ) & ( not A is empty & A is closed implies {d0} c= A ) ) thus ( {d0} c= A implies A is closed ) ::_thesis: ( not A is empty & A is closed implies {d0} c= A ) proof assume {d0} c= A ; ::_thesis: A is closed then A = A \/ {d0} by XBOOLE_1:12; then Cl A = A by A6; hence A is closed ; ::_thesis: verum end; thus ( not A is empty & A is closed implies {d0} c= A ) ::_thesis: verum proof assume not A is empty ; ::_thesis: ( not A is closed or {d0} c= A ) then A7: Cl A = A \/ {d0} by A6; assume A is closed ; ::_thesis: {d0} c= A then A8: Cl A = A by PRE_TOPC:22; assume not {d0} c= A ; ::_thesis: contradiction hence contradiction by A7, A8, XBOOLE_1:7; ::_thesis: verum end; end; hence TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) by A5, Th24; ::_thesis: verum end; theorem :: TEX_1:27 for D being non empty set for d0 being Element of D for Y being non empty TopSpace holds ( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) iff ( the carrier of Y = D & ( for A being Subset of Y st A <> D holds Int A = A \ {d0} ) ) ) proof let D be non empty set ; ::_thesis: for d0 being Element of D for Y being non empty TopSpace holds ( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) iff ( the carrier of Y = D & ( for A being Subset of Y st A <> D holds Int A = A \ {d0} ) ) ) let d0 be Element of D; ::_thesis: for Y being non empty TopSpace holds ( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) iff ( the carrier of Y = D & ( for A being Subset of Y st A <> D holds Int A = A \ {d0} ) ) ) let Y be non empty TopSpace; ::_thesis: ( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) iff ( the carrier of Y = D & ( for A being Subset of Y st A <> D holds Int A = A \ {d0} ) ) ) thus ( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) implies ( the carrier of Y = D & ( for A being Subset of Y st A <> D holds Int A = A \ {d0} ) ) ) ::_thesis: ( the carrier of Y = D & ( for A being Subset of Y st A <> D holds Int A = A \ {d0} ) implies TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) ) proof assume A1: TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) ; ::_thesis: ( the carrier of Y = D & ( for A being Subset of Y st A <> D holds Int A = A \ {d0} ) ) hence the carrier of Y = D ; ::_thesis: for A being Subset of Y st A <> D holds Int A = A \ {d0} reconsider P = {d0} as Subset of Y by A1; now__::_thesis:_for_A_being_Subset_of_Y_st_A_<>_D_holds_ Int_A_=_A_\_{d0} let A be Subset of Y; ::_thesis: ( A <> D implies Int A = A \ {d0} ) reconsider B = A as Subset of Y ; A2: A = A /\ D by A1, XBOOLE_1:28; assume A3: A <> D ; ::_thesis: Int A = A \ {d0} now__::_thesis:_not_Int_A_=_D assume Int A = D ; ::_thesis: contradiction then D c= A by TOPS_1:16; hence contradiction by A1, A3, XBOOLE_0:def_10; ::_thesis: verum end; then A4: Int A c= D \ P by A1, Th25; A \ {d0} c= D \ {d0} by A1, XBOOLE_1:33; then B \ P is open by A1, Th25; then Int (A \ P) = A \ P by TOPS_1:23; then A5: A \ {d0} c= Int A by TOPS_1:19, XBOOLE_1:36; Int A c= A by TOPS_1:16; then Int A c= A /\ (D \ P) by A4, XBOOLE_1:19; then Int A c= A \ {d0} by A2, XBOOLE_1:49; hence Int A = A \ {d0} by A5, XBOOLE_0:def_10; ::_thesis: verum end; hence for A being Subset of Y st A <> D holds Int A = A \ {d0} ; ::_thesis: verum end; assume A6: the carrier of Y = D ; ::_thesis: ( ex A being Subset of Y st ( A <> D & not Int A = A \ {d0} ) or TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) ) assume A7: for A being Subset of Y st A <> D holds Int A = A \ {d0} ; ::_thesis: TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) now__::_thesis:_for_A_being_Subset_of_Y_holds_ (_(_A_c=_D_\_{d0}_implies_A_is_open_)_&_(_A_<>_D_&_A_is_open_implies_A_c=_D_\_{d0}_)_) let A be Subset of Y; ::_thesis: ( ( A c= D \ {d0} implies A is open ) & ( A <> D & A is open implies A c= D \ {d0} ) ) thus ( A c= D \ {d0} implies A is open ) ::_thesis: ( A <> D & A is open implies A c= D \ {d0} ) proof assume A8: A c= D \ {d0} ; ::_thesis: A is open A9: now__::_thesis:_not_A_=_D D /\ {d0} = {d0} by ZFMISC_1:46; then A10: D meets {d0} by XBOOLE_0:def_7; assume A = D ; ::_thesis: contradiction then D = D \ {d0} by A8, XBOOLE_0:def_10; hence contradiction by A10, XBOOLE_1:83; ::_thesis: verum end; A11: A = A /\ D by A6, XBOOLE_1:28; A = A /\ (D \ {d0}) by A8, XBOOLE_1:28; then A = A \ {d0} by A11, XBOOLE_1:49; then Int A = A by A7, A9; hence A is open ; ::_thesis: verum end; thus ( A <> D & A is open implies A c= D \ {d0} ) ::_thesis: verum proof assume A12: A <> D ; ::_thesis: ( not A is open or A c= D \ {d0} ) assume A is open ; ::_thesis: A c= D \ {d0} then Int A = A by TOPS_1:23; then A \ {d0} = A by A7, A12; hence A c= D \ {d0} by A6, XBOOLE_1:33; ::_thesis: verum end; end; hence TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (STS (D,d0)), the topology of (STS (D,d0)) #) by A6, Th25; ::_thesis: verum end; Lm2: now__::_thesis:_for_D_being_non_empty_set_ for_d0_being_Element_of_D for_G_being_set_st_G_=__{__P_where_P_is_Subset_of_D_:_(_d0_in_P_&_P_<>_D_)__}__&_D_=_{d0}_holds_ not_G_<>_{} let D be non empty set ; ::_thesis: for d0 being Element of D for G being set st G = { P where P is Subset of D : ( d0 in P & P <> D ) } & D = {d0} holds not G <> {} let d0 be Element of D; ::_thesis: for G being set st G = { P where P is Subset of D : ( d0 in P & P <> D ) } & D = {d0} holds not G <> {} let G be set ; ::_thesis: ( G = { P where P is Subset of D : ( d0 in P & P <> D ) } & D = {d0} implies not G <> {} ) assume A1: G = { P where P is Subset of D : ( d0 in P & P <> D ) } ; ::_thesis: ( D = {d0} implies not G <> {} ) set x = the Element of G; assume A2: D = {d0} ; ::_thesis: not G <> {} assume G <> {} ; ::_thesis: contradiction then the Element of G in G ; then consider S being Subset of D such that the Element of G = S and A3: d0 in S and A4: S <> D by A1; set d1 = the Element of D \ S; A5: now__::_thesis:_not_D_\_S_=_{} assume D \ S = {} ; ::_thesis: contradiction then D c= S by XBOOLE_1:37; hence contradiction by A4, XBOOLE_0:def_10; ::_thesis: verum end; then reconsider d1 = the Element of D \ S as Element of D by XBOOLE_0:def_5; d0 <> d1 by A3, A5, XBOOLE_0:def_5; hence contradiction by A2, TARSKI:def_1; ::_thesis: verum end; theorem :: TEX_1:28 for D being non empty set for d0 being Element of D holds ( STS (D,d0) = ADTS D iff D = {d0} ) proof let D be non empty set ; ::_thesis: for d0 being Element of D holds ( STS (D,d0) = ADTS D iff D = {d0} ) let d0 be Element of D; ::_thesis: ( STS (D,d0) = ADTS D iff D = {d0} ) set G = { P where P is Subset of D : ( d0 in P & P <> D ) } ; thus ( STS (D,d0) = ADTS D implies D = {d0} ) ::_thesis: ( D = {d0} implies STS (D,d0) = ADTS D ) proof set d1 = the Element of D \ {d0}; assume A1: STS (D,d0) = ADTS D ; ::_thesis: D = {d0} assume A2: D <> {d0} ; ::_thesis: contradiction A3: now__::_thesis:_not_D_\_{d0}_=_{} assume D \ {d0} = {} ; ::_thesis: contradiction then D c= {d0} by XBOOLE_1:37; hence contradiction by A2, XBOOLE_0:def_10; ::_thesis: verum end; then reconsider d1 = the Element of D \ {d0} as Element of D by XBOOLE_0:def_5; reconsider P = {d1} as Subset of D ; A4: d0 <> d1 by A3, ZFMISC_1:56; then for Q being Subset of D holds ( not Q = P or not d0 in Q or not Q <> D ) by TARSKI:def_1; then not P in { P where P is Subset of D : ( d0 in P & P <> D ) } ; then A5: P in {{},D} by A1, XBOOLE_0:def_5; {d0} c= D ; then {d0} c= {d1} by A5, TARSKI:def_2; hence contradiction by A4, ZFMISC_1:18; ::_thesis: verum end; assume A6: D = {d0} ; ::_thesis: STS (D,d0) = ADTS D then { P where P is Subset of D : ( d0 in P & P <> D ) } = {} by Lm2; hence STS (D,d0) = ADTS D by A6, ZFMISC_1:24; ::_thesis: verum end; theorem :: TEX_1:29 for D being non empty set for d0 being Element of D holds ( STS (D,d0) = 1TopSp D iff D = {d0} ) proof let D be non empty set ; ::_thesis: for d0 being Element of D holds ( STS (D,d0) = 1TopSp D iff D = {d0} ) let d0 be Element of D; ::_thesis: ( STS (D,d0) = 1TopSp D iff D = {d0} ) set G = { P where P is Subset of D : ( d0 in P & P <> D ) } ; thus ( STS (D,d0) = 1TopSp D implies D = {d0} ) ::_thesis: ( D = {d0} implies STS (D,d0) = 1TopSp D ) proof now__::_thesis:_for_x_being_set_st_x_in__{__P_where_P_is_Subset_of_D_:_(_d0_in_P_&_P_<>_D_)__}__holds_ x_in_bool_D let x be set ; ::_thesis: ( x in { P where P is Subset of D : ( d0 in P & P <> D ) } implies x in bool D ) assume x in { P where P is Subset of D : ( d0 in P & P <> D ) } ; ::_thesis: x in bool D then ex Q being Subset of D st ( x = Q & d0 in Q & Q <> D ) ; hence x in bool D ; ::_thesis: verum end; then A1: { P where P is Subset of D : ( d0 in P & P <> D ) } c= bool D by TARSKI:def_3; reconsider P = {d0} as Subset of D ; assume A2: STS (D,d0) = 1TopSp D ; ::_thesis: D = {d0} A3: d0 in P by TARSKI:def_1; assume D <> {d0} ; ::_thesis: contradiction then P in { P where P is Subset of D : ( d0 in P & P <> D ) } by A3; hence contradiction by A2, A1, XBOOLE_1:38; ::_thesis: verum end; assume D = {d0} ; ::_thesis: STS (D,d0) = 1TopSp D then { P where P is Subset of D : ( d0 in P & P <> D ) } = {} by Lm2; hence STS (D,d0) = 1TopSp D ; ::_thesis: verum end; theorem :: TEX_1:30 for D being non empty set for d0 being Element of D for A being Subset of (STS (D,d0)) st A = {d0} holds 1TopSp D = (STS (D,d0)) modified_with_respect_to A proof let D be non empty set ; ::_thesis: for d0 being Element of D for A being Subset of (STS (D,d0)) st A = {d0} holds 1TopSp D = (STS (D,d0)) modified_with_respect_to A let d0 be Element of D; ::_thesis: for A being Subset of (STS (D,d0)) st A = {d0} holds 1TopSp D = (STS (D,d0)) modified_with_respect_to A set G = { P where P is Subset of D : ( d0 in P & P <> D ) } ; set T = (bool D) \ { P where P is Subset of D : ( d0 in P & P <> D ) } ; let A be Subset of (STS (D,d0)); ::_thesis: ( A = {d0} implies 1TopSp D = (STS (D,d0)) modified_with_respect_to A ) assume A1: A = {d0} ; ::_thesis: 1TopSp D = (STS (D,d0)) modified_with_respect_to A A2: A -extension_of_the_topology_of (STS (D,d0)) = { (H \/ (F /\ A)) where H, F is Subset of (STS (D,d0)) : ( H in (bool D) \ { P where P is Subset of D : ( d0 in P & P <> D ) } & F in (bool D) \ { P where P is Subset of D : ( d0 in P & P <> D ) } ) } by TMAP_1:def_7; now__::_thesis:_for_W_being_set_st_W_in__{__P_where_P_is_Subset_of_D_:_(_d0_in_P_&_P_<>_D_)__}__holds_ W_in_A_-extension_of_the_topology_of_(STS_(D,d0)) reconsider F = D as Subset of D by Lm1; let W be set ; ::_thesis: ( W in { P where P is Subset of D : ( d0 in P & P <> D ) } implies W in A -extension_of_the_topology_of (STS (D,d0)) ) assume W in { P where P is Subset of D : ( d0 in P & P <> D ) } ; ::_thesis: W in A -extension_of_the_topology_of (STS (D,d0)) then consider P being Subset of D such that A3: W = P and A4: d0 in P and P <> D ; set H = P \ {d0}; reconsider H = P \ {d0} as Subset of D ; A c= P by A1, A4, ZFMISC_1:31; then A5: W = H \/ A by A1, A3, XBOOLE_1:45; for K being Subset of D holds ( not K = F or not d0 in K or not K <> D ) ; then not F in { P where P is Subset of D : ( d0 in P & P <> D ) } ; then A6: F in (bool D) \ { P where P is Subset of D : ( d0 in P & P <> D ) } by XBOOLE_0:def_5; d0 in {d0} by TARSKI:def_1; then for K being Subset of D holds ( not K = H or not d0 in K or not K <> D ) by XBOOLE_0:def_5; then not H in { P where P is Subset of D : ( d0 in P & P <> D ) } ; then A7: H in (bool D) \ { P where P is Subset of D : ( d0 in P & P <> D ) } by XBOOLE_0:def_5; A = F /\ A by XBOOLE_1:28; hence W in A -extension_of_the_topology_of (STS (D,d0)) by A2, A6, A7, A5; ::_thesis: verum end; then A8: { P where P is Subset of D : ( d0 in P & P <> D ) } c= A -extension_of_the_topology_of (STS (D,d0)) by TARSKI:def_3; ((bool D) \ { P where P is Subset of D : ( d0 in P & P <> D ) } ) \/ { P where P is Subset of D : ( d0 in P & P <> D ) } = (bool D) \/ { P where P is Subset of D : ( d0 in P & P <> D ) } by XBOOLE_1:39; then A9: bool D c= ((bool D) \ { P where P is Subset of D : ( d0 in P & P <> D ) } ) \/ { P where P is Subset of D : ( d0 in P & P <> D ) } by XBOOLE_1:7; (bool D) \ { P where P is Subset of D : ( d0 in P & P <> D ) } c= A -extension_of_the_topology_of (STS (D,d0)) by TMAP_1:88; then ((bool D) \ { P where P is Subset of D : ( d0 in P & P <> D ) } ) \/ { P where P is Subset of D : ( d0 in P & P <> D ) } c= A -extension_of_the_topology_of (STS (D,d0)) by A8, XBOOLE_1:8; then A10: bool D c= A -extension_of_the_topology_of (STS (D,d0)) by A9, XBOOLE_1:1; the topology of ((STS (D,d0)) modified_with_respect_to A) = A -extension_of_the_topology_of (STS (D,d0)) by TMAP_1:93 .= the topology of (1TopSp D) by A10, XBOOLE_0:def_10 ; hence 1TopSp D = (STS (D,d0)) modified_with_respect_to A by TMAP_1:93; ::_thesis: verum end; begin definition let X be non empty TopSpace; redefine attr X is discrete means :Def5: :: TEX_1:def 5 for A being non empty Subset of X holds not A is boundary ; compatibility ( X is discrete iff for A being non empty Subset of X holds not A is boundary ) proof hereby ::_thesis: ( ( for A being non empty Subset of X holds not A is boundary ) implies X is discrete ) assume A1: X is discrete ; ::_thesis: for A being non empty Subset of X holds not A is boundary let A be non empty Subset of X; ::_thesis: not A is boundary assume A is boundary ; ::_thesis: contradiction then Int A <> A ; then not A is open by TOPS_1:23; hence contradiction by A1, TDLAT_3:15; ::_thesis: verum end; assume A2: for A being non empty Subset of X holds not A is boundary ; ::_thesis: X is discrete now__::_thesis:_for_A_being_Subset_of_X for_x_being_Point_of_X_st_A_=_{x}_holds_ A_is_open let A be Subset of X; ::_thesis: for x being Point of X st A = {x} holds A is open let x be Point of X; ::_thesis: ( A = {x} implies A is open ) assume A3: A = {x} ; ::_thesis: A is open hereby ::_thesis: verum percases ( A = {} or A <> {} ) ; suppose A = {} ; ::_thesis: A is open hence A is open ; ::_thesis: verum end; suppose A <> {} ; ::_thesis: A is open then not A is boundary by A2; then A4: Int A <> {} by TOPS_1:48; Int A c= {x} by A3, TOPS_1:16; hence A is open by A3, A4, ZFMISC_1:33; ::_thesis: verum end; end; end; end; hence X is discrete by TDLAT_3:17; ::_thesis: verum end; end; :: deftheorem Def5 defines discrete TEX_1:def_5_:_ for X being non empty TopSpace holds ( X is discrete iff for A being non empty Subset of X holds not A is boundary ); theorem :: TEX_1:31 for X being non empty TopSpace holds ( X is discrete iff for A being Subset of X st A <> the carrier of X holds not A is dense ) proof let X be non empty TopSpace; ::_thesis: ( X is discrete iff for A being Subset of X st A <> the carrier of X holds not A is dense ) hereby ::_thesis: ( ( for A being Subset of X st A <> the carrier of X holds not A is dense ) implies X is discrete ) assume A1: X is discrete ; ::_thesis: for A being Subset of X st A <> the carrier of X holds not A is dense assume ex A being Subset of X st ( A <> the carrier of X & A is dense ) ; ::_thesis: contradiction then consider A being Subset of X such that A2: A <> the carrier of X and A3: A is dense ; now__::_thesis:_ex_B_being_non_empty_Subset_of_X_st_B_is_boundary reconsider B = A ` as non empty Subset of X by A2, TOPS_3:2; take B = B; ::_thesis: B is boundary thus B is boundary by A3, TOPS_3:18; ::_thesis: verum end; hence contradiction by A1, Def5; ::_thesis: verum end; assume A4: for C being Subset of X st C <> the carrier of X holds not C is dense ; ::_thesis: X is discrete assume not X is discrete ; ::_thesis: contradiction then consider A being non empty Subset of X such that A5: A is boundary by Def5; now__::_thesis:_ex_B_being_Element_of_K10(_the_carrier_of_X)_st_ (_B_<>_the_carrier_of_X_&_B_is_dense_) take B = A ` ; ::_thesis: ( B <> the carrier of X & B is dense ) thus ( B <> the carrier of X & B is dense ) by A5, TOPS_1:def_4, TOPS_3:1; ::_thesis: verum end; hence contradiction by A4; ::_thesis: verum end; registration cluster non empty TopSpace-like non almost_discrete -> non empty non discrete non anti-discrete for TopStruct ; coherence for b1 being non empty TopSpace st not b1 is almost_discrete holds ( not b1 is discrete & not b1 is anti-discrete ) ; end; definition let X be non empty TopSpace; redefine attr X is almost_discrete means :Def6: :: TEX_1:def 6 for A being non empty Subset of X holds not A is nowhere_dense ; compatibility ( X is almost_discrete iff for A being non empty Subset of X holds not A is nowhere_dense ) proof hereby ::_thesis: ( ( for A being non empty Subset of X holds not A is nowhere_dense ) implies X is almost_discrete ) assume A1: X is almost_discrete ; ::_thesis: for A being non empty Subset of X holds not A is nowhere_dense let A be non empty Subset of X; ::_thesis: not A is nowhere_dense Cl A is open by A1, TDLAT_3:22; then Cl A = Int (Cl A) by TOPS_1:23; then Int (Cl A) <> {} by PRE_TOPC:18, XBOOLE_1:3; hence not A is nowhere_dense by TOPS_3:def_3; ::_thesis: verum end; assume A2: for A being non empty Subset of X holds not A is nowhere_dense ; ::_thesis: X is almost_discrete now__::_thesis:_for_A_being_Subset_of_X for_x_being_Point_of_X_st_A_=_{x}_holds_ Cl_A_is_open let A be Subset of X; ::_thesis: for x being Point of X st A = {x} holds Cl A is open let x be Point of X; ::_thesis: ( A = {x} implies Cl A is open ) assume A = {x} ; ::_thesis: Cl A is open hereby ::_thesis: verum Fr (Cl A) = {} by A2; then (Cl A) \ (Int (Cl A)) = {} by TOPS_1:43; then A3: Cl A c= Int (Cl A) by XBOOLE_1:37; Int (Cl A) c= Cl A by TOPS_1:16; hence Cl A is open by A3, XBOOLE_0:def_10; ::_thesis: verum end; end; hence X is almost_discrete by TDLAT_3:25; ::_thesis: verum end; end; :: deftheorem Def6 defines almost_discrete TEX_1:def_6_:_ for X being non empty TopSpace holds ( X is almost_discrete iff for A being non empty Subset of X holds not A is nowhere_dense ); theorem Th32: :: TEX_1:32 for X being non empty TopSpace holds ( X is almost_discrete iff for A being Subset of X st A <> the carrier of X holds not A is everywhere_dense ) proof let X be non empty TopSpace; ::_thesis: ( X is almost_discrete iff for A being Subset of X st A <> the carrier of X holds not A is everywhere_dense ) hereby ::_thesis: ( ( for A being Subset of X st A <> the carrier of X holds not A is everywhere_dense ) implies X is almost_discrete ) assume A1: X is almost_discrete ; ::_thesis: for A being Subset of X st A <> the carrier of X holds not A is everywhere_dense assume ex A being Subset of X st ( A <> the carrier of X & A is everywhere_dense ) ; ::_thesis: contradiction then consider A being Subset of X such that A2: A is everywhere_dense and A3: A <> the carrier of X ; now__::_thesis:_ex_B_being_non_empty_Subset_of_X_st_B_is_nowhere_dense reconsider B = A ` as non empty Subset of X by A3, TOPS_3:2; take B = B; ::_thesis: B is nowhere_dense thus B is nowhere_dense by A2, TOPS_3:39; ::_thesis: verum end; hence contradiction by A1, Def6; ::_thesis: verum end; assume A4: for A being Subset of X st A <> the carrier of X holds not A is everywhere_dense ; ::_thesis: X is almost_discrete assume not X is almost_discrete ; ::_thesis: contradiction then consider A being non empty Subset of X such that A5: A is nowhere_dense by Def6; now__::_thesis:_ex_B_being_Element_of_K10(_the_carrier_of_X)_st_ (_B_<>_the_carrier_of_X_&_B_is_everywhere_dense_) take B = A ` ; ::_thesis: ( B <> the carrier of X & B is everywhere_dense ) thus ( B <> the carrier of X & B is everywhere_dense ) by A5, TOPS_3:1, TOPS_3:40; ::_thesis: verum end; hence contradiction by A4; ::_thesis: verum end; theorem Th33: :: TEX_1:33 for X being non empty TopSpace holds ( not X is almost_discrete iff ex A being non empty Subset of X st ( A is boundary & A is closed ) ) proof let X be non empty TopSpace; ::_thesis: ( not X is almost_discrete iff ex A being non empty Subset of X st ( A is boundary & A is closed ) ) thus ( not X is almost_discrete implies ex A being non empty Subset of X st ( A is boundary & A is closed ) ) ::_thesis: ( ex A being non empty Subset of X st ( A is boundary & A is closed ) implies not X is almost_discrete ) proof assume not X is almost_discrete ; ::_thesis: ex A being non empty Subset of X st ( A is boundary & A is closed ) then consider A being non empty Subset of X such that A1: A is nowhere_dense by Def6; consider C being Subset of X such that A2: A c= C and A3: C is closed and A4: C is boundary by A1, TOPS_3:27; reconsider C = C as non empty Subset of X by A2; reconsider C = C as non empty Subset of X ; take C ; ::_thesis: ( C is boundary & C is closed ) thus ( C is boundary & C is closed ) by A3, A4; ::_thesis: verum end; given A being non empty Subset of X such that A5: A is boundary and A6: A is closed ; ::_thesis: not X is almost_discrete thus not X is almost_discrete by A5, A6, Def6; ::_thesis: verum end; theorem :: TEX_1:34 for X being non empty TopSpace holds ( not X is almost_discrete iff ex A being Subset of X st ( A <> the carrier of X & A is dense & A is open ) ) proof let X be non empty TopSpace; ::_thesis: ( not X is almost_discrete iff ex A being Subset of X st ( A <> the carrier of X & A is dense & A is open ) ) thus ( not X is almost_discrete implies ex A being Subset of X st ( A <> the carrier of X & A is dense & A is open ) ) ::_thesis: ( ex A being Subset of X st ( A <> the carrier of X & A is dense & A is open ) implies not X is almost_discrete ) proof assume not X is almost_discrete ; ::_thesis: ex A being Subset of X st ( A <> the carrier of X & A is dense & A is open ) then consider A being non empty Subset of X such that A1: A is boundary and A2: A is closed by Th33; take A ` ; ::_thesis: ( A ` <> the carrier of X & A ` is dense & A ` is open ) thus ( A ` <> the carrier of X & A ` is dense & A ` is open ) by A1, A2, TOPS_3:1; ::_thesis: verum end; given A being Subset of X such that A3: A <> the carrier of X and A4: A is dense and A5: A is open ; ::_thesis: not X is almost_discrete now__::_thesis:_ex_B_being_non_empty_Subset_of_X_st_ (_B_is_boundary_&_B_is_closed_) reconsider B = A ` as non empty Subset of X by A3, TOPS_3:2; take B = B; ::_thesis: ( B is boundary & B is closed ) thus ( B is boundary & B is closed ) by A4, A5, TOPS_3:18; ::_thesis: verum end; hence not X is almost_discrete by Th33; ::_thesis: verum end; registration cluster non empty strict TopSpace-like non discrete non anti-discrete almost_discrete for TopStruct ; existence ex b1 being TopSpace st ( b1 is almost_discrete & not b1 is discrete & not b1 is anti-discrete & b1 is strict & not b1 is empty ) proof set C = bool {{},1}; set Y = ADTS (bool {{},1}); A1: 1 in {{},1} by TARSKI:def_2; {} in {{},1} by TARSKI:def_2; then reconsider B0 = {{}}, B1 = {1} as Subset of {{},1} by A1, ZFMISC_1:31; A2: {} c= {{},1} by XBOOLE_1:2; then reconsider A = {{}} as Subset of (ADTS (bool {{},1})) by ZFMISC_1:31; set Y1 = (ADTS (bool {{},1})) modified_with_respect_to A; A3: the carrier of ((ADTS (bool {{},1})) modified_with_respect_to A) = the carrier of (ADTS (bool {{},1})) by TMAP_1:93; reconsider A1 = A as Subset of ((ADTS (bool {{},1})) modified_with_respect_to A) by TMAP_1:93; set Y2 = ((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `); reconsider A2 = A1 as Subset of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) by TMAP_1:93; set A3 = A2 ` ; A4: the carrier of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) = the carrier of ((ADTS (bool {{},1})) modified_with_respect_to A) by TMAP_1:93; then reconsider B = {B0,B1} as non empty Subset of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) by TMAP_1:93; now__::_thesis:_for_H_being_set_st_H_in_the_topology_of_((ADTS_(bool_{{},1}))_modified_with_respect_to_A)_holds_ H_in_{{},A1,(bool_{{},1})} let H be set ; ::_thesis: ( H in the topology of ((ADTS (bool {{},1})) modified_with_respect_to A) implies H in {{},A1,(bool {{},1})} ) assume H in the topology of ((ADTS (bool {{},1})) modified_with_respect_to A) ; ::_thesis: H in {{},A1,(bool {{},1})} then H in A -extension_of_the_topology_of (ADTS (bool {{},1})) by TMAP_1:93; then H in { (p \/ (q /\ A)) where p, q is Subset of (ADTS (bool {{},1})) : ( p in the topology of (ADTS (bool {{},1})) & q in the topology of (ADTS (bool {{},1})) ) } by TMAP_1:def_7; then consider P, Q being Subset of (ADTS (bool {{},1})) such that A5: H = P \/ (Q /\ A) and A6: P in the topology of (ADTS (bool {{},1})) and A7: Q in the topology of (ADTS (bool {{},1})) ; now__::_thesis:_(_(_P_=_{}_&_Q_=_{}_&_H_=_{}_)_or_(_P_=_bool_{{},1}_&_Q_=_{}_&_H_=_bool_{{},1}_)_or_(_P_=_{}_&_Q_=_bool_{{},1}_&_H_=_A_)_or_(_P_=_bool_{{},1}_&_Q_=_bool_{{},1}_&_H_=_bool_{{},1}_)_) percases ( ( P = {} & Q = {} ) or ( P = bool {{},1} & Q = {} ) or ( P = {} & Q = bool {{},1} ) or ( P = bool {{},1} & Q = bool {{},1} ) ) by A6, A7, TARSKI:def_2; case ( P = {} & Q = {} ) ; ::_thesis: H = {} hence H = {} by A5; ::_thesis: verum end; case ( P = bool {{},1} & Q = {} ) ; ::_thesis: H = bool {{},1} hence H = bool {{},1} by A5; ::_thesis: verum end; case ( P = {} & Q = bool {{},1} ) ; ::_thesis: H = A hence H = A by A5, XBOOLE_1:28; ::_thesis: verum end; case ( P = bool {{},1} & Q = bool {{},1} ) ; ::_thesis: H = bool {{},1} hence H = bool {{},1} by A5, XBOOLE_1:12; ::_thesis: verum end; end; end; hence H in {{},A1,(bool {{},1})} by ENUMSET1:def_1; ::_thesis: verum end; then A8: the topology of ((ADTS (bool {{},1})) modified_with_respect_to A) c= {{},A1,(bool {{},1})} by TARSKI:def_3; now__::_thesis:_for_H_being_set_st_H_in_the_topology_of_(((ADTS_(bool_{{},1}))_modified_with_respect_to_A)_modified_with_respect_to_(A1_`))_holds_ H_in_{{},A2,(A2_`),(bool_{{},1})} let H be set ; ::_thesis: ( H in the topology of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) implies H in {{},A2,(A2 `),(bool {{},1})} ) assume H in the topology of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) ; ::_thesis: H in {{},A2,(A2 `),(bool {{},1})} then H in (A1 `) -extension_of_the_topology_of ((ADTS (bool {{},1})) modified_with_respect_to A) by TMAP_1:93; then H in { (P \/ (Q /\ (A1 `))) where P, Q is Subset of ((ADTS (bool {{},1})) modified_with_respect_to A) : ( P in the topology of ((ADTS (bool {{},1})) modified_with_respect_to A) & Q in the topology of ((ADTS (bool {{},1})) modified_with_respect_to A) ) } by TMAP_1:def_7; then consider P, Q being Subset of ((ADTS (bool {{},1})) modified_with_respect_to A) such that A9: H = P \/ (Q /\ (A1 `)) and A10: P in the topology of ((ADTS (bool {{},1})) modified_with_respect_to A) and A11: Q in the topology of ((ADTS (bool {{},1})) modified_with_respect_to A) ; now__::_thesis:_(_(_P_=_{}_&_Q_=_{}_&_H_=_{}_)_or_(_P_=_A1_&_Q_=_{}_&_H_=_A1_)_or_(_P_=_bool_{{},1}_&_Q_=_{}_&_H_=_bool_{{},1}_)_or_(_P_=_{}_&_Q_=_A1_&_H_=_{}_)_or_(_P_=_A1_&_Q_=_A1_&_H_=_A1_)_or_(_P_=_bool_{{},1}_&_Q_=_A1_&_H_=_bool_{{},1}_)_or_(_P_=_{}_&_Q_=_bool_{{},1}_&_H_=_A2_`_)_or_(_P_=_A1_&_Q_=_bool_{{},1}_&_H_=_bool_{{},1}_)_or_(_P_=_bool_{{},1}_&_Q_=_bool_{{},1}_&_H_=_bool_{{},1}_)_) percases ( ( P = {} & Q = {} ) or ( P = A1 & Q = {} ) or ( P = bool {{},1} & Q = {} ) or ( P = {} & Q = A1 ) or ( P = A1 & Q = A1 ) or ( P = bool {{},1} & Q = A1 ) or ( P = {} & Q = bool {{},1} ) or ( P = A1 & Q = bool {{},1} ) or ( P = bool {{},1} & Q = bool {{},1} ) ) by A8, A10, A11, ENUMSET1:def_1; case ( P = {} & Q = {} ) ; ::_thesis: H = {} hence H = {} by A9; ::_thesis: verum end; case ( P = A1 & Q = {} ) ; ::_thesis: H = A1 hence H = A1 by A9; ::_thesis: verum end; case ( P = bool {{},1} & Q = {} ) ; ::_thesis: H = bool {{},1} hence H = bool {{},1} by A9; ::_thesis: verum end; caseA12: ( P = {} & Q = A1 ) ; ::_thesis: H = {} A1 misses A1 ` by XBOOLE_1:79; hence H = {} by A9, A12, XBOOLE_0:def_7; ::_thesis: verum end; caseA13: ( P = A1 & Q = A1 ) ; ::_thesis: H = A1 A1 misses A1 ` by XBOOLE_1:79; then A1 /\ (A1 `) = {} ((ADTS (bool {{},1})) modified_with_respect_to A) by XBOOLE_0:def_7; hence H = A1 by A9, A13; ::_thesis: verum end; caseA14: ( P = bool {{},1} & Q = A1 ) ; ::_thesis: H = bool {{},1} A1 misses A1 ` by XBOOLE_1:79; then A1 /\ (A1 `) = {} ((ADTS (bool {{},1})) modified_with_respect_to A) by XBOOLE_0:def_7; hence H = bool {{},1} by A9, A14; ::_thesis: verum end; case ( P = {} & Q = bool {{},1} ) ; ::_thesis: H = A2 ` hence H = A2 ` by A3, A4, A9, XBOOLE_1:28; ::_thesis: verum end; caseA15: ( P = A1 & Q = bool {{},1} ) ; ::_thesis: H = bool {{},1} A1 \/ (A1 `) = [#] ((ADTS (bool {{},1})) modified_with_respect_to A) by PRE_TOPC:2; hence H = bool {{},1} by A3, A9, A15, XBOOLE_1:28; ::_thesis: verum end; case ( P = bool {{},1} & Q = bool {{},1} ) ; ::_thesis: H = bool {{},1} hence H = bool {{},1} by A3, A9, XBOOLE_1:12; ::_thesis: verum end; end; end; hence H in {{},A2,(A2 `),(bool {{},1})} by ENUMSET1:def_2; ::_thesis: verum end; then A16: the topology of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) c= {{},A2,(A2 `),(bool {{},1})} by TARSKI:def_3; A17: A2 is open by Th1, TMAP_1:94; A18: A2 is closed by Th3; now__::_thesis:_for_H_being_set_st_H_in_{{},A2,(A2_`),(bool_{{},1})}_holds_ H_in_the_topology_of_(((ADTS_(bool_{{},1}))_modified_with_respect_to_A)_modified_with_respect_to_(A1_`)) let H be set ; ::_thesis: ( H in {{},A2,(A2 `),(bool {{},1})} implies H in the topology of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) ) assume H in {{},A2,(A2 `),(bool {{},1})} ; ::_thesis: H in the topology of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) then ( H = {} or H = A2 or H = A2 ` or H = bool {{},1} ) by ENUMSET1:def_2; hence H in the topology of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) by A3, A4, A18, A17, PRE_TOPC:1, PRE_TOPC:def_1, PRE_TOPC:def_2; ::_thesis: verum end; then {{},A2,(A2 `),(bool {{},1})} c= the topology of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) by TARSKI:def_3; then A19: the topology of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) = {{},A2,(A2 `),(bool {{},1})} by A16, XBOOLE_0:def_10; A20: now__::_thesis:_for_G_being_Subset_of_(((ADTS_(bool_{{},1}))_modified_with_respect_to_A)_modified_with_respect_to_(A1_`))_st_G_is_open_holds_ G_is_closed let G be Subset of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)); ::_thesis: ( G is open implies G is closed ) A21: now__::_thesis:_(_(_G_=_{}_or_G_=_bool_{{},1}_)_implies_G_is_closed_) assume ( G = {} or G = bool {{},1} ) ; ::_thesis: G is closed then ( G = {} (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) or G = [#] (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) ) by A4, TMAP_1:93; hence G is closed ; ::_thesis: verum end; A22: now__::_thesis:_(_G_=_A2_implies_G_is_closed_) A2 ` in the topology of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) by A19, ENUMSET1:def_2; then A23: A2 ` is open by PRE_TOPC:def_2; assume G = A2 ; ::_thesis: G is closed hence G is closed by A23, TOPS_1:3; ::_thesis: verum end; A24: now__::_thesis:_(_G_=_A2_`_implies_G_is_closed_) A2 in the topology of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) by A19, ENUMSET1:def_2; then A25: (A2 `) ` is open by PRE_TOPC:def_2; assume G = A2 ` ; ::_thesis: G is closed hence G is closed by A25; ::_thesis: verum end; assume G is open ; ::_thesis: G is closed then G in {{},A2,(A2 `),(bool {{},1})} by A19, PRE_TOPC:def_2; hence G is closed by A21, A22, A24, ENUMSET1:def_2; ::_thesis: verum end; A26: {} in bool {{},1} by A2; A27: now__::_thesis:_ex_B_being_non_empty_Subset_of_(((ADTS_(bool_{{},1}))_modified_with_respect_to_A)_modified_with_respect_to_(A1_`))_st_B_is_boundary A28: now__::_thesis:_not_Int_B_=_A2_` reconsider I = {{},1} as Point of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) by A3, A4, ZFMISC_1:def_1; A29: not I in A2 by TARSKI:def_1; A30: Int B c= B by TOPS_1:16; assume Int B = A2 ` ; ::_thesis: contradiction then I in Int B by A29, SUBSET_1:29; then ( I = B0 or I = B1 ) by A30, TARSKI:def_2; then ( 1 in B0 or {} in B1 ) by TARSKI:def_2; hence contradiction by TARSKI:def_1; ::_thesis: verum end; take B = B; ::_thesis: B is boundary A31: now__::_thesis:_not_Int_B_=_A2 assume Int B = A2 ; ::_thesis: contradiction then A32: {} in Int B by TARSKI:def_1; Int B c= B by TOPS_1:16; hence contradiction by A32, TARSKI:def_2; ::_thesis: verum end; A33: now__::_thesis:_not_Int_B_=_bool_{{},1} assume Int B = bool {{},1} ; ::_thesis: contradiction then bool {{},1} c= B by TOPS_1:16; hence contradiction by A26, TARSKI:def_2; ::_thesis: verum end; Int B in {{},A2,(A2 `),(bool {{},1})} by A19, PRE_TOPC:def_2; then ( Int B = {} or Int B = A2 or Int B = A2 ` or Int B = bool {{},1} ) by ENUMSET1:def_2; hence B is boundary by A33, A31, A28, TOPS_1:48; ::_thesis: verum end; take ((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `) ; ::_thesis: ( ((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `) is almost_discrete & not ((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `) is discrete & not ((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `) is anti-discrete & ((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `) is strict & not ((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `) is empty ) now__::_thesis:_ex_A2_being_Subset_of_(((ADTS_(bool_{{},1}))_modified_with_respect_to_A)_modified_with_respect_to_(A1_`))_st_ (_A2_is_open_&_A2_<>_{}_&_A2_<>_the_carrier_of_(((ADTS_(bool_{{},1}))_modified_with_respect_to_A)_modified_with_respect_to_(A1_`))_) take A2 = A2; ::_thesis: ( A2 is open & A2 <> {} & A2 <> the carrier of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) ) now__::_thesis:_not_A2_=_bool_{{},1} assume A2 = bool {{},1} ; ::_thesis: contradiction then B0 = {} by TARSKI:def_1; hence contradiction ; ::_thesis: verum end; hence ( A2 is open & A2 <> {} & A2 <> the carrier of (((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `)) ) by A4, Th1, TMAP_1:93, TMAP_1:94; ::_thesis: verum end; hence ( ((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `) is almost_discrete & not ((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `) is discrete & not ((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `) is anti-discrete & ((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `) is strict & not ((ADTS (bool {{},1})) modified_with_respect_to A) modified_with_respect_to (A1 `) is empty ) by A27, A20, Def5, TDLAT_3:18, TDLAT_3:21; ::_thesis: verum end; end; theorem Th35: :: TEX_1:35 for C being non empty set for c0 being Element of C holds ( not C \ {c0} is empty iff not STS (C,c0) is almost_discrete ) proof let C be non empty set ; ::_thesis: for c0 being Element of C holds ( not C \ {c0} is empty iff not STS (C,c0) is almost_discrete ) let c0 be Element of C; ::_thesis: ( not C \ {c0} is empty iff not STS (C,c0) is almost_discrete ) hereby ::_thesis: ( not STS (C,c0) is almost_discrete implies not C \ {c0} is empty ) assume A1: not C \ {c0} is empty ; ::_thesis: not STS (C,c0) is almost_discrete now__::_thesis:_ex_A_being_non_empty_Subset_of_(STS_(C,c0))_st_A_is_nowhere_dense reconsider A = {c0} as non empty Subset of (STS (C,c0)) ; take A = A; ::_thesis: A is nowhere_dense A2: A is boundary by A1, Th21; A is closed by A1, Th21; hence A is nowhere_dense by A2; ::_thesis: verum end; hence not STS (C,c0) is almost_discrete by Def6; ::_thesis: verum end; assume not STS (C,c0) is almost_discrete ; ::_thesis: not C \ {c0} is empty then consider A being non empty Subset of (STS (C,c0)) such that A3: A is nowhere_dense by Def6; assume C \ {c0} is empty ; ::_thesis: contradiction then C c= {c0} by XBOOLE_1:37; then C = {c0} by XBOOLE_0:def_10; then A = C by ZFMISC_1:33; hence contradiction by A3, TOPS_3:23; ::_thesis: verum end; registration cluster non empty strict TopSpace-like non almost_discrete for TopStruct ; existence ex b1 being TopSpace st ( not b1 is almost_discrete & b1 is strict & not b1 is empty ) proof set D = {{},1}; reconsider a = {} as Element of {{},1} by TARSKI:def_2; set Y = STS ({{},1},a); take STS ({{},1},a) ; ::_thesis: ( not STS ({{},1},a) is almost_discrete & STS ({{},1},a) is strict & not STS ({{},1},a) is empty ) reconsider A = {a} as non empty Subset of (STS ({{},1},a)) ; A1: not 1 in A by TARSKI:def_1; 1 in {{},1} by TARSKI:def_2; then not {{},1} \ A is empty by A1, XBOOLE_0:def_5; hence ( not STS ({{},1},a) is almost_discrete & STS ({{},1},a) is strict & not STS ({{},1},a) is empty ) by Th35; ::_thesis: verum end; end; theorem :: TEX_1:36 for X being non empty TopSpace for A being non empty Subset of X st A is boundary holds not X modified_with_respect_to (A `) is almost_discrete proof let X be non empty TopSpace; ::_thesis: for A being non empty Subset of X st A is boundary holds not X modified_with_respect_to (A `) is almost_discrete let A be non empty Subset of X; ::_thesis: ( A is boundary implies not X modified_with_respect_to (A `) is almost_discrete ) set Z = X modified_with_respect_to (A `); assume A1: A is boundary ; ::_thesis: not X modified_with_respect_to (A `) is almost_discrete now__::_thesis:_ex_C_being_non_empty_Subset_of_(X_modified_with_respect_to_(A_`))_st_C_is_nowhere_dense reconsider C = A as non empty Subset of (X modified_with_respect_to (A `)) by TMAP_1:93; take C = C; ::_thesis: C is nowhere_dense thus C is nowhere_dense by A1, Th7; ::_thesis: verum end; hence not X modified_with_respect_to (A `) is almost_discrete by Def6; ::_thesis: verum end; theorem :: TEX_1:37 for X being non empty TopSpace for A being Subset of X st A <> the carrier of X & A is dense holds not X modified_with_respect_to A is almost_discrete proof let X be non empty TopSpace; ::_thesis: for A being Subset of X st A <> the carrier of X & A is dense holds not X modified_with_respect_to A is almost_discrete let A be Subset of X; ::_thesis: ( A <> the carrier of X & A is dense implies not X modified_with_respect_to A is almost_discrete ) assume A1: A <> the carrier of X ; ::_thesis: ( not A is dense or not X modified_with_respect_to A is almost_discrete ) set Z = X modified_with_respect_to A; assume A2: A is dense ; ::_thesis: not X modified_with_respect_to A is almost_discrete now__::_thesis:_ex_C_being_Subset_of_(X_modified_with_respect_to_A)_st_ (_C_<>_the_carrier_of_(X_modified_with_respect_to_A)_&_C_is_everywhere_dense_) reconsider C = A as Subset of (X modified_with_respect_to A) by TMAP_1:93; take C = C; ::_thesis: ( C <> the carrier of (X modified_with_respect_to A) & C is everywhere_dense ) thus ( C <> the carrier of (X modified_with_respect_to A) & C is everywhere_dense ) by A1, A2, Th5, TMAP_1:93; ::_thesis: verum end; hence not X modified_with_respect_to A is almost_discrete by Th32; ::_thesis: verum end;