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