Copyright (c) 1993 Association of Mizar Users
environ
vocabulary PRE_TOPC, TMAP_1, SUBSET_1, BOOLE, TOPS_1, TOPS_3, REALSET1,
SETFAM_1, TDLAT_3, NATTRA_1, TARSKI, TEX_1, PCOMPS_1;
notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, SETFAM_1, STRUCT_0, REALSET1,
PRE_TOPC, TOPS_1, TMAP_1, TDLAT_3, TOPS_3, PCOMPS_1;
constructors REALSET1, TOPS_1, TMAP_1, TDLAT_3, TOPS_3, DOMAIN_1, PCOMPS_1,
MEMBERED;
clusters TDLAT_3, STRUCT_0, COMPLSP1, TMAP_1, SUBSET_1, TOPS_1, PCOMPS_1,
XBOOLE_0, ZFMISC_1;
requirements BOOLE, SUBSET;
definitions PRE_TOPC, TDLAT_3, STRUCT_0;
theorems TARSKI, SUBSET_1, ZFMISC_1, ENUMSET1, REALSET1, PRE_TOPC, TOPS_1,
PCOMPS_1, TMAP_1, TDLAT_1, TDLAT_3, TOPS_3, STRUCT_0, SETFAM_1, XBOOLE_0,
XBOOLE_1, TSEP_1;
begin
:: 1. Properties of Subsets of a Topological Space with Modified Topology.
reserve X for non empty TopSpace, D for Subset of X;
theorem Th1:
for B being Subset of X,
C being Subset of X modified_with_respect_to D st
B = C holds B is open implies C is open
proof let B be Subset of X,
C be Subset of X modified_with_respect_to D;
assume A1: B = C;
assume A2: B in the topology of X;
the topology of X c= D-extension_of_the_topology_of X &
the topology of X modified_with_respect_to D =
D-extension_of_the_topology_of X by TMAP_1:99,104;
hence C is open by A1,A2,PRE_TOPC:def 5;
end;
theorem
for B being Subset of X,
C being Subset of X modified_with_respect_to D st
B = C holds B is closed implies C is closed
proof let B be Subset of X,
C be Subset of X modified_with_respect_to D;
assume A1: B = C;
assume B is closed;
then A2: B` is open by TOPS_1:29;
the carrier of (X modified_with_respect_to D) = the carrier of X
by TMAP_1:104;
then B` = C` by A1;
then C` is open by A2,Th1;
hence C is closed by TOPS_1:29;
end;
Lm1:
for X be non empty TopSpace, D be Subset of X,
C be Subset of X modified_with_respect_to D`
st C = D holds C` = D` by TMAP_1:104;
theorem Th3:
for C being Subset of X modified_with_respect_to D` st C = D holds
C is closed
proof let C be Subset of X modified_with_respect_to D`;
assume C = D;
then C` = D` by Lm1;
then C` is open by TMAP_1:105;
hence thesis by TOPS_1:29;
end;
theorem Th4:
for C being Subset of X modified_with_respect_to D
st C = D holds
D is dense implies C is dense & C is open
proof let C be Subset of X modified_with_respect_to D;
assume A1: C = D;
assume A2: D is dense;
set A = (Cl C)`;
A is Subset of X by TMAP_1:104;
then reconsider B = A as Subset of X;
A in the topology of (X modified_with_respect_to D) by PRE_TOPC:def 5;
then A in D-extension_of_the_topology_of X by TMAP_1:104;
then A in {H \/ (G /\ D) where H is Subset of X,
G is Subset of X :
H in the topology of X & G in
the topology of X} by TMAP_1:def 7;
then consider H, G being Subset of X such that
A3: A = H \/ (G /\ D) and A4: H in the topology of X and
G in the topology of X;
A5: C c= Cl C by PRE_TOPC:48;
then D misses A & G /\ D c= D by A1,TOPS_1:20,XBOOLE_1:17;
then (G /\ D) misses A by XBOOLE_1:63;
then A6: (G /\ D) /\ A = {} by XBOOLE_0:def 7;
A = (H \/ (G /\ D)) /\ A by A3
.= (H /\ A) \/ {} by A6,XBOOLE_1:23
.= H /\ A;
then A c= H & H c= A by A3,XBOOLE_1:7,17;
then B = H by XBOOLE_0:def 10;
then B is open & D misses B by A1,A4,A5,PRE_TOPC:def 5,TOPS_1:20;
then (Cl D) misses B & Cl D = [#]X by A2,TOPS_1:def 3,TSEP_1:40;
then A7: (Cl D) /\ B = {} & Cl D = [#]X by XBOOLE_0:def 7;
thus C is dense
proof
assume C is not dense;
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 A7,PRE_TOPC:15;
end;
thus C is open by A1,TMAP_1:105;
end;
theorem Th5:
for C being Subset of X modified_with_respect_to D
st D c= C holds
D is dense implies C is everywhere_dense
proof let C be Subset of X modified_with_respect_to D;
assume A1: D c= C;
assume A2: D is dense;
D is Subset of X modified_with_respect_to D
by TMAP_1:104;
then reconsider E = D as Subset of X modified_with_respect_to D
;
E is dense & E is open by A2,Th4;
then E is everywhere_dense & E c= C by A1,TOPS_3:36;
hence thesis by TOPS_3:38;
end;
theorem Th6:
for C being Subset of X modified_with_respect_to D`
st C = D holds
D is boundary implies C is boundary & C is closed
proof let C be Subset of X modified_with_respect_to D`;
assume C = D;
then A1: C` = D` by Lm1;
assume D is boundary;
then D` is dense by TOPS_1:def 4;
then C` is dense & C` is open by A1,Th4;
hence thesis by TOPS_1:29,def 4;
end;
theorem Th7:
for C being Subset of X modified_with_respect_to D`
st C c= D holds
D is boundary implies C is nowhere_dense
proof let C be Subset of X modified_with_respect_to D`;
assume A1: C c= D;
assume A2: D is boundary;
D is Subset of X modified_with_respect_to D`
by TMAP_1:104;
then reconsider
E = D as Subset of X modified_with_respect_to D`
;
E is boundary & E is closed by A2,Th6;
then E is nowhere_dense & C c= E by A1,TOPS_1:93;
hence thesis by TOPS_3:26;
end;
Lm2: for X,Y be set holds X c= Y iff X is Subset of Y;
begin
:: 2. Trivial Topological Spaces.
definition let Y be non empty 1-sorted;
redefine attr Y is trivial means
:Def1: ex d being Element of Y st the carrier of Y = {d};
compatibility
proof
hereby assume A1: Y is trivial;
thus ex d being Element of Y st the carrier of Y = {d}
proof
reconsider A = the carrier of Y as Subset of Y by Lm2;
consider d being Element of Y;
reconsider D = {d} as Subset of Y;
take d;
now let a be Element of Y;
assume a in A;
a = d by A1,REALSET1:def 20;
hence a in D by TARSKI:def 1;
end;
then A c= D & D c= A by SUBSET_1:7;
hence the carrier of Y = {d} by XBOOLE_0:def 10;
end;
end;
given d being Element of Y such that
A2: the carrier of Y = {d};
now let a,b be Element of Y;
a = d & b = d by A2,TARSKI:def 1;
hence a = b;
end;
hence Y is trivial by REALSET1:def 20;
end;
end;
definition let A be non empty set;
cluster 1-sorted(#A#) -> non empty;
coherence by STRUCT_0:def 1;
end;
definition
cluster trivial strict non empty 1-sorted;
existence
proof
take Y = 1-sorted (#{0}#);
now
reconsider d = 0 as Element of Y by TARSKI:def 1;
take d;
thus the carrier of Y = {d};
end;
hence thesis by Def1;
end;
cluster non trivial strict non empty 1-sorted;
existence
proof
take Y = 1-sorted (#{0,1}#);
now assume Y is trivial;
then consider d being Element of Y such that
A1: the carrier of Y = {d} by Def1;
thus contradiction by A1,ZFMISC_1:9;
end;
hence thesis;
end;
end;
definition
cluster trivial strict non empty TopStruct;
existence
proof
consider O being trivial strict non empty 1-sorted;
reconsider tau = {} as Subset of bool the carrier of O by XBOOLE_1:2;
reconsider tau as Subset-Family of O by SETFAM_1:def 7;
take Y = TopStruct (#the carrier of O,tau#);
now
consider d being Element of O such that
A1: the carrier of O = {d} by Def1;
reconsider d as Element of Y;
take d;
thus the carrier of Y = {d} by A1;
end;
hence thesis by Def1;
end;
cluster non trivial strict non empty TopStruct;
existence
proof
consider O being non trivial strict non empty 1-sorted;
reconsider tau = {} as Subset of bool the carrier of O by XBOOLE_1:2;
reconsider tau as Subset-Family of O by SETFAM_1:def 7;
take Y = TopStruct (#the carrier of O,tau#);
now assume Y is trivial;
then ex d being Element of Y st
the carrier of Y = {d} by Def1;
hence contradiction by Def1;
end;
hence thesis;
end;
end;
theorem
for Y being trivial non empty TopStruct st the topology of Y is non empty
holds Y is almost_discrete implies Y is TopSpace-like
proof let Y be trivial non empty TopStruct;
consider d being Element of Y such that
A1: the carrier of Y = {d} by Def1;
reconsider D = {d} as Subset of Y;
A2: bool D = {{},D} by ZFMISC_1:30;
assume the topology of Y is non empty;
then consider A being Subset of Y such that
A3: A in the topology of Y by SUBSET_1:10;
assume A4: for A being Subset of Y st
A in the topology of Y holds
(the carrier of Y) \ A in the topology of Y;
now per cases by A1,A2,TARSKI:def 2;
suppose A5: A = {};
D \ A in the topology of Y by A1,A3,A4;
hence {{},D} c= the topology of Y by A3,A5,ZFMISC_1:38;
suppose A6: A = D;
D \ A in the topology of Y by A1,A3,A4;
then {} in the topology of Y by A6,XBOOLE_1:37;
hence {{},D} c= the topology of Y by A3,A6,ZFMISC_1:38;
end;
then the topology of Y = {{}, the carrier of Y} by A1,A2,XBOOLE_0:def 10;
then reconsider Y as anti-discrete TopStruct by TDLAT_3:def 2;
Y is TopSpace-like;
hence thesis;
end;
definition
cluster trivial strict non empty TopSpace;
existence
proof
consider O being trivial strict non empty 1-sorted;
reconsider tau = bool the carrier of O as
Subset of bool the carrier of O;
reconsider tau as Subset-Family of O;
set Y = TopStruct (#the carrier of O,tau#);
A1: now
consider d being Element of O such that
A2: the carrier of O = {d} by Def1;
reconsider d as Element of Y;
take d;
thus the carrier of Y = {d} by A2;
end;
reconsider Y as discrete non empty TopStruct by TDLAT_3:def 1;
reconsider Y as TopSpace-like non empty TopStruct;
take Y;
thus thesis by A1,Def1;
end;
end;
definition
cluster trivial -> anti-discrete discrete (non empty TopSpace);
coherence
proof let Y be non empty TopSpace;
assume Y is trivial;
then consider d being Element of Y such that
A1: the carrier of Y = {d} by Def1;
{} in the topology of Y & the carrier of Y in the topology of Y
by PRE_TOPC:5,def 1;
then A2: {{}, the carrier of Y} c= the topology of Y by ZFMISC_1:38;
A3: bool the carrier of Y = {{}, the carrier of Y} by A1,ZFMISC_1:30;
then the topology of Y = bool the carrier of Y by A2,XBOOLE_0:def 10;
hence thesis by A3,TDLAT_3:def 1,def 2;
end;
cluster discrete anti-discrete -> trivial (non empty TopSpace);
coherence
proof let Y be non empty TopSpace;
assume Y is discrete anti-discrete;
then A4: bool the carrier of Y = {{}, the carrier of Y} by TDLAT_3:12;
now
consider d0 being Element of Y;
take d0;
thus {d0} = the carrier of Y by A4,TARSKI:def 2;
end;
hence Y is trivial by Def1;
end;
end;
definition
cluster non trivial strict non empty TopSpace;
existence
proof
set D = {0,1};
reconsider tau = bool D as Subset of bool D;
reconsider tau as Subset-Family of D;
reconsider Y=TopStruct (#D,tau#) as discrete non empty TopStruct
by TDLAT_3:def 1;
take Y;
now assume Y is trivial;
then consider d being Element of Y such that
A1: the carrier of Y = {d} by Def1;
d = 0 & d = 1 by A1,ZFMISC_1:8;
hence contradiction;
end;
hence thesis;
end;
end;
definition
cluster non discrete -> non trivial (non empty TopSpace);
coherence
proof let Y be non empty TopSpace;
assume A1: Y is non discrete;
now assume Y is trivial;
then reconsider Y as trivial non empty TopSpace;
Y is discrete;
hence contradiction by A1;
end;
hence thesis;
end;
cluster non anti-discrete -> non trivial (non empty TopSpace);
coherence
proof let Y be non empty TopSpace;
assume A2: Y is non anti-discrete;
now assume Y is trivial;
then reconsider Y as trivial non empty TopSpace;
Y is anti-discrete;
hence contradiction by A2;
end;
hence thesis;
end;
end;
begin
:: 3. Examples of Discrete and Anti-discrete Topological Spaces.
definition let D be set;
func cobool D -> Subset-Family of D equals
:Def2: {{},D};
coherence
proof
{} c= D & D in bool D by XBOOLE_1:2,ZFMISC_1:def 1;
then {{},D} is Subset of bool D by ZFMISC_1:38;
hence thesis by SETFAM_1:def 7;
end;
end;
definition let D be set;
cluster cobool D -> non empty;
coherence
proof
cobool D = {{},D} by Def2;
hence thesis;
end;
end;
definition let D be set;
func ADTS(D) -> TopStruct equals
:Def3: TopStruct(#D,cobool D#);
coherence;
end;
definition let D be set;
cluster ADTS(D) -> strict anti-discrete TopSpace-like;
coherence
proof
set Y = TopStruct (#D,cobool D#);
the topology of Y = {{},the carrier of Y} by Def2;
then reconsider Y' = Y as anti-discrete TopStruct by TDLAT_3:def 2;
Y' is anti-discrete strict TopSpace;
hence thesis by Def3;
end;
end;
definition let D be non empty set;
cluster ADTS(D) -> non empty;
coherence
proof ADTS(D) = TopStruct(#D,cobool D#) by Def3;
hence thesis;
end;
end;
theorem Th9:
for X being anti-discrete non empty TopSpace holds
the TopStruct of X = ADTS(the carrier of X)
proof let X be anti-discrete non empty TopSpace;
A1: ADTS(the carrier of X) =
TopStruct (#the carrier of X,cobool the carrier of X#) by Def3;
the topology of X = {{},the carrier of X} by TDLAT_3:def 2
.= the topology of ADTS(the carrier of X) by A1,Def2;
hence thesis by A1;
end;
theorem
for X being non empty TopSpace st
the TopStruct of X = the TopStruct of ADTS(the carrier of X) holds
X is anti-discrete
proof let X be non empty TopSpace;
assume A1: the TopStruct of X = the TopStruct of ADTS(the carrier of X);
ADTS(the carrier of X) =
TopStruct (#the carrier of X,cobool the carrier of X#) by Def3;
then the topology of X = {{},the carrier of X} by A1,Def2;
hence X is anti-discrete by TDLAT_3:def 2;
end;
theorem Th11:
for X being anti-discrete non empty TopSpace
for A being Subset of X holds (A is empty implies Cl A = {}) &
(A is non empty implies Cl A = the carrier of X)
proof let X be anti-discrete non empty TopSpace;
let A be Subset of X;
thus A is empty implies Cl A = {}
proof
assume A is empty;
then A = {}X;
hence thesis by PRE_TOPC:52;
end;
thus A is non empty implies Cl A = the carrier of X
proof
assume A is non empty;
then Cl A <> {} by PCOMPS_1:2;
hence thesis by TDLAT_3:21;
end;
end;
theorem Th12:
for X being anti-discrete non empty 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 anti-discrete non empty TopSpace;
let A be Subset of X;
thus A <> the carrier of X implies Int A = {}
proof
assume A1: A <> the carrier of X;
now assume Int A = the carrier of X;
then the carrier of X c= A &
A c= the carrier of X by TOPS_1:44;
hence contradiction by A1,XBOOLE_0:def 10;
end;
hence thesis by TDLAT_3:20;
end;
thus A = the carrier of X implies Int A = the carrier of X
proof
assume A = the carrier of X;
then A = [#]X by PRE_TOPC:12;
then Int A = [#]X by TOPS_1:43;
hence thesis by PRE_TOPC:12;
end;
end;
theorem Th13:
for X being non empty TopSpace holds
(for A being Subset of X holds
(A is non empty implies Cl A = the carrier of X))
implies X is anti-discrete
proof let X be non empty TopSpace;
assume A1: for A being Subset of X holds
(A is non empty implies Cl A = the carrier of X);
now let A be Subset of X;
assume A is closed;
then A = Cl A & (A <> {} iff A is non empty) by PRE_TOPC:52;
hence A = {} or A = the carrier of X by A1;
end;
hence thesis by TDLAT_3:21;
end;
theorem Th14:
for X being non empty TopSpace holds
(for A being Subset of X
holds (A <> the carrier of X implies Int A = {}))
implies X is anti-discrete
proof let X be non empty TopSpace;
assume A1: for A being Subset of X holds
(A <> the carrier of X implies Int A = {});
now let A be Subset of X;
assume A is open;
then A = Int A by TOPS_1:55;
hence A = {} or A = the carrier of X by A1;
end;
hence thesis by TDLAT_3:20;
end;
theorem
for X being anti-discrete non empty 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 anti-discrete non empty TopSpace;
let A be Subset of X;
thus A <> {} implies A is dense
proof
assume A <> {};
then Cl A = the carrier of X by Th11;
hence thesis by TOPS_3:def 2;
end;
thus A <> the carrier of X implies A is boundary
proof
assume A <> the carrier of X;
then Int A = {} by Th12;
hence thesis by TOPS_1:84;
end;
end;
theorem
for X being non empty TopSpace holds
(for A being Subset of X holds (A <> {} implies A is dense))
implies X is anti-discrete
proof let X be non empty TopSpace;
assume A1: for A being Subset of X holds (A <> {} implies A is dense);
now let A be Subset of X;
reconsider B = A as Subset of X;
assume A is non empty;
then B is dense by A1;
hence Cl A = the carrier of X by TOPS_3:def 2;
end;
hence thesis by Th13;
end;
theorem
for X being non empty TopSpace holds
(for A being Subset of X
holds (A <> the carrier of X implies A is boundary))
implies X is anti-discrete
proof let X be non empty TopSpace;
assume A1: for A being Subset of X holds
(A <> the carrier of X implies A is boundary);
now let A be Subset of X;
reconsider B = A as Subset of X;
assume A <> the carrier of X;
then B is boundary by A1;
hence Int A = {} by TOPS_1:84;
end;
hence thesis by Th14;
end;
definition let D be set;
cluster 1TopSp D -> discrete;
coherence
proof
set Y = TopStruct (#D,bool D#);
reconsider Y' = Y as discrete TopStruct by TDLAT_3:def 1;
Y' is discrete strict TopSpace;
hence thesis by PCOMPS_1:def 1;
end;
end;
theorem Th18:
for X being discrete non empty TopSpace holds
the TopStruct of X = 1TopSp (the carrier of X)
proof let X be discrete non empty TopSpace;
1TopSp(the carrier of X) =
TopStruct (#the carrier of X,bool the carrier of X#) by PCOMPS_1:def 1;
hence thesis by TDLAT_3:def 1;
end;
theorem
for X being non empty TopSpace st
the TopStruct of X = the TopStruct of 1TopSp(the carrier of X) holds
X is discrete
proof let X be non empty TopSpace;
assume A1: the TopStruct of X = the TopStruct of 1TopSp(the carrier of X);
1TopSp(the carrier of X) =
TopStruct (#the carrier of X,bool the carrier of X#) by PCOMPS_1:def 1;
hence X is discrete by A1,TDLAT_3:def 1;
end;
theorem
for X being discrete non empty TopSpace
for A being Subset of X holds Cl A = A & Int A = A
proof let X be discrete non empty TopSpace;
let A be Subset of X;
reconsider B = A as Subset of X;
B is open & B is closed by TDLAT_3:17,18;
hence thesis by PRE_TOPC:52,TOPS_1:55;
end;
theorem
for X being non empty TopSpace holds
(for A being Subset of X holds Cl A = A) implies X is discrete
proof let X be non empty TopSpace;
assume A1: for A being Subset of X holds Cl A = A;
now let A be Subset of X;
Cl A = A by A1;
hence A is closed;
end;
hence thesis by TDLAT_3:18;
end;
theorem
for X being non empty TopSpace holds
(for A being Subset of X
holds Int A = A) implies X is discrete
proof let X be non empty TopSpace;
assume A1: for A being Subset of X holds Int A = A;
now let A be Subset of X;
Int A = A by A1;
hence A is open;
end;
hence thesis by TDLAT_3:17;
end;
theorem Th23:
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;
A1: 1TopSp(D) = TopStruct (#D,bool D#) by PCOMPS_1:def 1;
A2: ADTS(D) = TopStruct (#D,cobool D#) by Def3;
thus ADTS(D) = 1TopSp(D) implies ex d0 being Element of D st D = {d0}
proof
assume ADTS(D) = 1TopSp(D);
then A3: bool D = {{},D} by A1,TDLAT_3:12;
consider d0 being Element of D;
take d0;
{d0} c= D by ZFMISC_1:37;
hence thesis by A3,TARSKI:def 2;
end;
given d0 being Element of D such that A4: D = {d0};
bool D = {{},D} by A4,ZFMISC_1:30
.= cobool D by Def2;
hence thesis by A2,PCOMPS_1:def 1;
end;
definition
cluster discrete non anti-discrete strict non empty TopSpace;
existence
proof
set D = {0,1}; set Y = 1TopSp(D);
take Y;
A1: Y = TopStruct (#D,bool D#) by PCOMPS_1:def 1;
now assume Y is anti-discrete;
then the TopStruct of Y = the TopStruct of ADTS(D) by A1,Th9;
then consider d0 being Element of D such that A2: D = {d0} by Th23;
d0 = 0 & d0 = 1 by A2,ZFMISC_1:8;
hence contradiction;
end;
hence thesis;
end;
cluster anti-discrete non discrete strict non empty TopSpace;
existence
proof
set D = {0,1}; set Y = ADTS(D);
take Y;
A3: Y = TopStruct (#D,cobool D#) by Def3;
now assume Y is discrete;
then the TopStruct of Y = the TopStruct of 1TopSp(D) by A3,Th18;
then consider d0 being Element of D such that A4: D = {d0} by Th23;
d0 = 0 & d0 = 1 by A4,ZFMISC_1:8;
hence contradiction;
end;
hence thesis;
end;
end;
begin
:: 4. An Example of a Topological Space.
definition let D be set, F be Subset-Family of D, S be set;
redefine func F \ S -> Subset-Family of D;
coherence
proof set G = F \ S;
G c= F & F c= bool D by XBOOLE_1:36;
then G is Subset of bool D by XBOOLE_1:1;
hence thesis by SETFAM_1:def 7;
end;
end;
definition let D be set, d0 be Element of D;
canceled;
func STS(D,d0) -> TopStruct equals :Def5:
TopStruct (#D,(bool D) \ {A where A is Subset of D : d0 in A & A <> D}#);
coherence;
end;
definition let D be set, d0 be Element of D;
cluster STS(D,d0) -> strict TopSpace-like;
coherence
proof
set G = {A where A is Subset of D : d0 in A & A <> D};
set T = (bool D) \ G;
A1: T misses G by XBOOLE_1:79;
set Y = TopStruct (#D,T#);
A2: Y = STS(D,d0) by Def5;
hence STS(D,d0) is strict;
reconsider E = D as Subset of D by Lm2;
not ex A being Subset of D st A = E & d0 in A & A <> D;
then A3: not E in G;
then A4: the carrier of Y in the topology of Y by XBOOLE_0:def 4;
A5: now let F be Subset-Family of Y;
assume F c= the topology of Y;
then F c= bool D & F misses G by A1,XBOOLE_1:63;
then A6: F c= bool D & F /\ G = {} by XBOOLE_0:def 7;
now per cases;
case union F = D;
hence union F in the topology of Y by A3,XBOOLE_0:def 4;
case A7: union F <> D;
A8: now let A be Subset of D;
assume A9: A in F;
assume A = D;
then D c= union F by A9,ZFMISC_1:92;
hence contradiction by A7,XBOOLE_0:def 10;
end;
now let A be set;
assume A10: A in F;
then reconsider B = A as Subset of D;
not B in G by A6,A10,XBOOLE_0:def 3;
then not (d0 in B & B <> D);
hence not d0 in A by A8,A10;
end;
then not ex A being set st d0 in A & A in F;
then not ex A being Subset of D
st A = union F & d0 in A & A <> D by TARSKI:def 4;
then not union F in G;
hence union F in the topology of Y by XBOOLE_0:def 4;
end;
hence union F in the topology of Y;
end;
now let C,E be Subset of Y;
assume A11: C in the topology of Y & E in the topology of Y;
A12: now let P be Subset of D;
assume A13: P in the topology of Y & P <> D;
then not P in G by XBOOLE_0:def 4;
hence not d0 in P by A13;
end;
now per cases;
case C = D & E = D;
hence C /\ E in the topology of Y by A3,XBOOLE_0:def 4;
case A14: C <> D or E <> D;
now per cases by A14;
case C <> D;
then not d0 in C & C /\ E c= C by A11,A12,XBOOLE_1:17;
then not ex A being Subset of D st
A = C /\ E & d0 in A & A <> D;
then not C /\ E in G;
hence C /\ E in the topology of Y by XBOOLE_0:def 4;
case E <> D;
then not d0 in E & C /\ E c= E by A11,A12,XBOOLE_1:17;
then not ex A being Subset of D st
A = C /\ E & d0 in A & A <> D;
then not C /\ E in G;
hence C /\ E in the topology of Y by XBOOLE_0:def 4;
end;
hence C /\ E in the topology of Y;
end;
hence C /\ E in the topology of Y;
end;
hence thesis by A2,A4,A5,PRE_TOPC:def 1;
end;
end;
definition let D be non empty set, d0 be Element of D;
cluster STS(D,d0) -> non empty;
coherence
proof
STS(D,d0) = TopStruct(#D,(bool D)
\ {A where A is Subset of D : d0 in A & A <> D}#) by Def5;
hence the carrier of STS(D,d0) is non empty;
end;
end;
reserve D for non empty set, d0 for Element of D;
theorem Th24:
for A being Subset of STS(D,d0) holds
({d0} c= A implies A is closed) &
(A is non empty & A is closed implies {d0} c= A)
proof let A be Subset of STS(D,d0);
set Z = A`;
set G = {P where P is Subset of D : d0 in P & P <> D};
A1: STS(D,d0) = TopStruct(#D,(bool D) \ G#) by Def5;
thus {d0} c= A implies A is closed
proof assume A2: {d0} c= A;
d0 in {d0} by TARSKI:def 1;
then not ex Q being Subset of D
st Q = Z & d0 in Q & Q <> D by A2,SUBSET_1:54;
then not Z in G;
then Z in the topology of STS(D,d0) by A1,XBOOLE_0:def 4;
then Z is open by PRE_TOPC:def 5;
hence A is closed by TOPS_1:29;
end;
assume A is non empty;
then A3: Z <> D by A1,TOPS_3:1;
assume A is closed;
then Z is open by TOPS_1:29;
then Z in the topology of STS(D,d0) by PRE_TOPC:def 5;
then not Z in G by A1,XBOOLE_0:def 4;
then not d0 in Z by A1,A3;
then d0 in A by A1,SUBSET_1:50;
hence {d0} c= A by ZFMISC_1:37;
end;
theorem Th25:
D \ {d0} is non empty implies
for A being Subset of STS(D,d0) holds
(A = {d0} implies A is closed & A is boundary) &
(A is non empty & A is closed & A is boundary implies A = {d0})
proof
assume A1: D \ {d0} is non empty;
let A be Subset of STS(D,d0);
set G = {P where P is Subset of D : d0 in P & P <> D};
A2: STS(D,d0) = TopStruct(#D,(bool D) \ G#) by Def5;
A3: Int A in the topology of STS(D,d0) by PRE_TOPC:def 5;
thus A = {d0} implies A is closed & A is boundary
proof
assume A4: A = {d0};
hence A is closed by Th24;
Int A c= A by TOPS_1:44;
then A5: Int A = {} or Int A = A by A4,ZFMISC_1:39;
now assume A6: Int A = A;
then A7: d0 in Int A by A4,TARSKI:def 1;
Int A <> D by A1,A4,A6,XBOOLE_1:37;
then Int A in G by A2,A7;
hence contradiction by A2,A3,XBOOLE_0:def 4;
end;
hence A is boundary by A5,TOPS_1:84;
end;
thus A is non empty & A is closed & A is boundary implies A = {d0}
proof
assume A is non empty & A is closed;
then A8: {d0} c= A by Th24;
set Z = A \ {d0};
A9: Z c= A by XBOOLE_1:36;
then Z is Subset of STS(D,d0) by XBOOLE_1:1;
then reconsider Z as Subset of STS(D,d0);
assume A is boundary;
then A10: Int A = {} by TOPS_1:84;
assume A11: A <> {d0};
A12: now
assume Z = {};
then A c= {d0} by XBOOLE_1:37;
hence contradiction by A8,A11,XBOOLE_0:def 10;
end;
d0 in {d0} by TARSKI:def 1;
then not ex Q being Subset of D
st Q = Z & d0 in Q & Q <> D by XBOOLE_0:def 4;
then not Z in G;
then Z in the topology of STS(D,d0) by A2,XBOOLE_0:def 4;
then Z is open by PRE_TOPC:def 5;
then Z c= Int A by A9,TOPS_1:56;
hence contradiction by A10,A12,XBOOLE_1:3;
end;
end;
theorem Th26:
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 A be Subset of STS(D,d0);
set Z = A`;
set T = (bool D) \
{P where P is Subset of D : d0 in P & P <> D};
A1: STS(D,d0) = TopStruct(#D,T#) by Def5;
then A2: [#]STS(D,d0) = D by PRE_TOPC:12;
reconsider P = {d0} as Subset of STS(D,d0)
by A1,ZFMISC_1:37;
thus A c= D \ {d0} implies A is open
proof
assume A c= D \ {d0};
then [#]STS(D,d0) \ (D \ {d0}) c= [#]STS(D,d0) \ A by XBOOLE_1:34;
then [#]STS(D,d0) \ (D \ P) c= Z by PRE_TOPC:17;
then P c= Z by A2,PRE_TOPC:22;
then Z is closed by Th24;
hence thesis by TOPS_1:30;
end;
thus A <> D & A is open implies A c= D \ {d0}
proof
assume A <> D;
then A3: Z <> {}STS(D,d0) by A1,TOPS_3:2;
assume A is open;
then Z is closed by TOPS_1:30;
then {d0} c= Z by A3,Th24;
then Z` c= P` by PRE_TOPC:19;
then A c= P`;
hence thesis by A2,PRE_TOPC:17;
end;
end;
theorem
D \ {d0} is non 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})
proof
assume A1: D \ {d0} is non empty;
let A be Subset of STS(D,d0);
set Z = A`;
set T = (bool D) \
{P where P is Subset of D : d0 in P & P <> D};
A2: STS(D,d0) = TopStruct(#D,T#) by Def5;
then A3: [#]STS(D,d0) = D by PRE_TOPC:12;
reconsider P = {d0} as Subset of STS(D,d0) by A2,ZFMISC_1:37;
thus A = D \ {d0} implies A is open & A is dense
proof
assume A4: A = D \ {d0};
hence A is open by Th26;
[#]STS(D,d0) \ ([#]STS(D,d0) \ P) = Z by A3,A4,PRE_TOPC:17;
then P = Z by PRE_TOPC:22;
then Z is closed & Z is boundary by A1,Th25;
hence thesis by TOPS_3:18;
end;
thus A <> D & A is open & A is dense implies A = D \ {d0}
proof
assume A <> D;
then A5: Z <> {}STS(D,d0) by A2,TOPS_3:2;
assume A is open;
then A6: Z is closed by TOPS_1:30;
assume A is dense;
then Z is boundary by TOPS_3:18;
then Z = {d0} by A1,A5,A6,Th25;
then A = P`;
hence thesis by A3,PRE_TOPC:17;
end;
end;
definition
cluster non anti-discrete non discrete strict non empty TopSpace;
existence
proof
set D = {0,1};
reconsider a = 0 as Element of D by TARSKI:def 2;
set Y = STS(D,a);
take Y;
A1: Y = TopStruct(#D,(bool D)
\ {A where A is Subset of D : a in A & A <> D}#) by Def5;
then {a} is non empty Subset of Y by ZFMISC_1:37;
then reconsider A = {a} as non empty Subset of Y;
A2: 1 in D & not 1 in A by TARSKI:def 1,def 2;
then D \ A is non empty by XBOOLE_0:def 4;
then A3: A is closed & A is boundary by Th25;
then Int A <> A by TOPS_1:84;
then A is not open by TOPS_1:55;
hence thesis by A1,A2,A3,TDLAT_3:17,21;
end;
end;
theorem Th28:
for Y being non empty TopSpace holds
the TopStruct of Y = the TopStruct of STS(D,d0) iff
the carrier of Y = D &
for A being Subset of Y
holds ({d0} c= A implies A is closed) &
(A is non empty & A is closed implies {d0} c= A)
proof let Y be non empty TopSpace;
set G = {P where P is Subset of D : d0 in P & P <> D};
set T = (bool D) \ G;
A1: STS(D,d0) = TopStruct(#D,T#) by Def5;
thus the TopStruct of Y = the TopStruct of STS(D,d0) implies
the carrier of Y = D &
for A being Subset of Y
holds ({d0} c= A implies A is closed) &
(A is non empty & A is closed implies {d0} c= A)
proof
assume A2: the TopStruct of Y = the TopStruct of STS(D,d0);
hence the carrier of Y = D by A1;
now let A be Subset of Y;
reconsider B = A as Subset of STS(D,d0) by A2;
thus {d0} c= A implies A is closed
proof
assume {d0} c= A;
then B is closed by Th24;
hence thesis by A2,TOPS_3:79;
end;
thus A is non empty & A is closed implies {d0} c= A
proof
assume A3: A is non empty;
assume A is closed;
then B is closed by A2,TOPS_3:79;
hence {d0} c= A by A3,Th24;
end;
end;
hence thesis;
end;
assume A4: the carrier of Y = D;
assume A5: for A being Subset of Y
holds ({d0} c= A implies A is closed) &
(A is non empty & A is closed implies {d0} c= A);
now let A be Subset of Y,
C be Subset of STS(D,d0);
assume A6: A = C;
A7: now assume A8: A is closed;
now per cases;
case A = {};
then C = {}STS(D,d0) by A6;
hence C is closed;
case A <> {};
then {d0} c= C by A5,A6,A8;
hence C is closed by Th24;
end;
hence C is closed;
end;
now assume A9: C is closed;
now per cases;
case C = {};
then A = {}Y by A6;
hence A is closed;
case C <> {};
then {d0} c= A by A6,A9,Th24;
hence A is closed by A5;
end;
hence A is closed;
end;
hence A is closed iff C is closed by A7;
end;
hence thesis by A1,A4,TOPS_3:73;
end;
theorem Th29:
for Y being non empty TopSpace holds
the TopStruct of Y = the TopStruct 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 Y be non empty TopSpace;
set G = {P where P is Subset of D : d0 in P & P <> D};
set T = (bool D) \ G;
A1: STS(D,d0) = TopStruct(#D,T#) by Def5;
thus the TopStruct of Y = the TopStruct 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})
proof
assume A2: the TopStruct of Y = the TopStruct of STS(D,d0);
hence the carrier of Y = D by A1;
let A be Subset of Y;
reconsider B = A as Subset of STS(D,d0) by A2;
thus A c= D \ {d0} implies A is open
proof
assume A c= D \ {d0};
then B is open by Th26;
hence thesis by A2,TOPS_3:76;
end;
thus A <> D & A is open implies A c= D \ {d0}
proof
assume A3: A <> D;
assume A is open;
then B is open by A2,TOPS_3:76;
hence thesis by A3,Th26;
end;
end;
assume A4: the carrier of Y = D;
assume A5: 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});
now let A be Subset of Y,
C be Subset of STS(D,d0);
assume A6: A = C;
A7: now assume A8: A is open;
now per cases;
case A = D;
then C = [#]STS(D,d0) by A1,A6,PRE_TOPC:12;
hence C is open;
case A <> D;
then A c= D \ {d0} by A5,A8;
hence C is open by A6,Th26;
end;
hence C is open;
end;
now assume A9: C is open;
now per cases;
case C = D;
then A = [#]Y by A4,A6,PRE_TOPC:12;
hence A is open;
case C <> D;
then A c= D \ {d0} by A6,A9,Th26;
hence A is open by A5;
end;
hence A is open;
end;
hence A is open iff C is open by A7;
end;
hence thesis by A1,A4,TOPS_3:72;
end;
theorem
for Y being non empty TopSpace holds
the TopStruct of Y = the TopStruct 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 Y be non empty TopSpace;
set G = {P where P is Subset of D : d0 in P & P <> D};
set T = (bool D) \ G;
A1: STS(D,d0) = TopStruct(#D,T#) by Def5;
thus the TopStruct of Y = the TopStruct of STS(D,d0) implies
the carrier of Y = D &
for A being non empty Subset of Y holds Cl A = A \/
{d0}
proof
assume A2: the TopStruct of Y = the TopStruct of STS(D,d0);
hence the carrier of Y = D by A1;
{d0} is Subset of Y by A1,A2,ZFMISC_1:37;
then reconsider P = {d0} as Subset of Y;
now let A be non empty Subset of Y;
reconsider B = A as Subset of Y;
{d0} c= A \/ P by XBOOLE_1:7;
then B \/ P is closed by A2,Th28;
then A3: Cl(A \/ P) = A \/ {d0} by PRE_TOPC:52;
A c= A \/ {d0} by XBOOLE_1:7;
then A4: Cl A c= Cl(A \/ P) by PRE_TOPC:49;
Cl A is non empty & Cl A is closed by PCOMPS_1:2;
then {d0} c= Cl A & A c= Cl A by A2,Th28,PRE_TOPC:48;
then A \/ {d0} c= Cl A by XBOOLE_1:8;
hence Cl A = A \/ {d0} by A3,A4,XBOOLE_0:def 10;
end;
hence thesis;
end;
assume A5: the carrier of Y = D;
assume A6: for A being non empty Subset of Y
holds Cl A = A \/ {d0};
now let A be Subset of Y;
thus {d0} c= A implies A is closed
proof
assume {d0} c= A;
then A = A \/ {d0} by XBOOLE_1:12;
then Cl A = A by A6;
hence thesis;
end;
thus A is non empty & A is closed implies {d0} c= A
proof
assume A7: A is non empty;
assume A8: A is closed;
assume A9: not {d0} c= A;
Cl A = A \/ {d0} & Cl A = A by A6,A7,A8,PRE_TOPC:52;
hence contradiction by A9,XBOOLE_1:7;
end;
end;
hence thesis by A5,Th28;
end;
theorem
for Y being non empty TopSpace holds
the TopStruct of Y = the TopStruct 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 Y be non empty TopSpace;
set G = {P where P is Subset of D : d0 in P & P <> D};
set T = (bool D) \ G;
A1: STS(D,d0) = TopStruct(#D,T#) by Def5;
thus the TopStruct of Y = the TopStruct of STS(D,d0) implies
the carrier of Y = D &
for A being Subset of Y st A <> D
holds Int A = A \ {d0}
proof
assume A2: the TopStruct of Y = the TopStruct of STS(D,d0);
hence the carrier of Y = D by A1;
reconsider P = {d0} as Subset of Y by A1,A2,ZFMISC_1:37;
now let A be Subset of Y;
reconsider B = A as Subset of Y;
assume A3: A <> D;
A \ {d0} c= D \ {d0} by A1,A2,XBOOLE_1:33;
then B \ P is open by A2,Th29;
then A4: Int(A \ P) = A \ P by TOPS_1:55;
A \ P c= A by XBOOLE_1:36;
then A5: A \ {d0} c= Int A by A4,TOPS_1:48;
now assume Int A = D;
then D c= A by TOPS_1:44;
hence contradiction by A1,A2,A3,XBOOLE_0:def 10;
end;
then Int A c= D \ P & Int A c= A by A2,Th29,TOPS_1:44;
then Int A c= A /\ (D \ P) & A = A /\ D by A1,A2,XBOOLE_1:19,28;
then Int A c= A \ {d0} by XBOOLE_1:49;
hence Int A = A \ {d0} by A5,XBOOLE_0:def 10;
end;
hence thesis;
end;
assume A6: the carrier of Y = D;
assume A7: for A being Subset of Y st A <> D
holds Int A = A \ {d0};
now let A be Subset of Y;
thus A c= D \ {d0} implies A is open
proof
assume A8: A c= D \ {d0};
A9: now assume A10: A = D;
D \ {d0} c= D by XBOOLE_1:36;
then A11: D = D \ {d0} by A8,A10,XBOOLE_0:def 10;
D /\ {d0} = {d0} & {d0} <> {} by ZFMISC_1:52;
then D meets {d0} by XBOOLE_0:def 7;
hence contradiction by A11,XBOOLE_1:83;
end;
A = A /\ (D \ {d0}) & A = A /\ D by A6,A8,XBOOLE_1:28;
then A = A \ {d0} by XBOOLE_1:49;
then Int A = A by A7,A9;
hence thesis;
end;
thus A <> D & A is open implies A c= D \ {d0}
proof
assume A12: A <> D;
assume A is open;
then Int A = A by TOPS_1:55;
then A \ {d0} = A & A c= D by A6,A7,A12;
hence thesis by XBOOLE_1:33;
end;
end;
hence thesis by A6,Th29;
end;
Lm3:
now let D be non empty set, d0 be Element of D, G be set;
assume A1: G = {P where P is Subset of D : d0 in P & P <> D};
assume A2: D = {d0};
assume A3: G <> {};
consider x being Element of G;
x in G by A3;
then consider S being Subset of D such that
x = S and A4: d0 in S and A5: S <> D by A1;
A6: now assume D \ S = {};
then D c= S by XBOOLE_1:37;
hence contradiction by A5,XBOOLE_0:def 10;
end;
consider d1 being Element of D \ S;
reconsider d1 as Element of D by A6,XBOOLE_0:def 4;
d0 <> d1 by A4,A6,XBOOLE_0:def 4;
hence contradiction by A2,TARSKI:def 1;
end;
theorem
STS(D,d0) = ADTS(D) iff D = {d0}
proof
A1: ADTS(D) = TopStruct (#D,cobool D#) by Def3;
set G = {P where P is Subset of D : d0 in P & P <> D};
set T = (bool D) \ G;
A2: STS(D,d0) = TopStruct(#D,T#) by Def5;
thus STS(D,d0) = ADTS(D) implies D = {d0}
proof
assume STS(D,d0) = ADTS(D);
then A3: {{},D} = T by A1,A2,Def2;
assume A4: D <> {d0};
A5: {d0} c= D by ZFMISC_1:37;
A6: now assume D \ {d0} = {};
then D c= {d0} by XBOOLE_1:37;
hence contradiction by A4,A5,XBOOLE_0:def 10;
end;
consider d1 being Element of D \ {d0};
reconsider d1 as Element of D by A6,XBOOLE_0:def 4;
A7: d0 <> d1 by A6,ZFMISC_1:64;
reconsider P = {d1} as Subset of D by ZFMISC_1:37;
not ex Q being Subset of D
st Q = P & d0 in Q & Q <> D by A7,TARSKI:def 1;
then not P in G;
then P in {{},D} by A3,XBOOLE_0:def 4;
then {d0} c= {d1} by A5,TARSKI:def 2;
hence contradiction by A7,ZFMISC_1:24;
end;
assume A8: D = {d0};
then G = {} by Lm3;
then T = {{},D} by A8,ZFMISC_1:30
.= cobool D by Def2;
hence thesis by A1,Def5;
end;
theorem
STS(D,d0) = 1TopSp(D) iff D = {d0}
proof
A1: 1TopSp(D) = TopStruct (#D,bool D#) by PCOMPS_1:def 1;
set G = {P where P is Subset of D : d0 in P & P <> D};
set T = (bool D) \ G;
A2: STS(D,d0) = TopStruct(#D,T#) by Def5;
thus STS(D,d0) = 1TopSp(D) implies D = {d0}
proof
assume A3: STS(D,d0) = 1TopSp(D);
A4: G c= bool D
proof
now let x be set;
assume x in G;
then consider Q being Subset of D such that
A5: x = Q and d0 in Q & Q <> D;
thus x in bool D by A5;
end;
hence thesis by TARSKI:def 3;
end;
assume A6: D <> {d0};
reconsider P = {d0} as Subset of D by ZFMISC_1:37;
d0 in P by TARSKI:def 1;
then P in G by A6;
hence contradiction by A1,A2,A3,A4,XBOOLE_1:38;
end;
assume D = {d0};
then G = {} by Lm3;
hence thesis by A2,PCOMPS_1:def 1;
end;
theorem
for D being non empty set, 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, d0 be Element of D;
A1: 1TopSp(D) = TopStruct(#D,bool D#) by PCOMPS_1:def 1;
set G = {P where P is Subset of D : d0 in P & P <> D};
set T = (bool D) \ G;
T \/ G = (bool D) \/ G by XBOOLE_1:39;
then A2: bool D c= T \/ G by XBOOLE_1:7;
A3: STS(D,d0) = TopStruct(#D,T#) by Def5;
let A be Subset of STS(D,d0);
assume A4: A = {d0};
A5: G c= A-extension_of_the_topology_of STS(D,d0)
proof
A6: A-extension_of_the_topology_of STS(D,d0) =
{H \/ (F /\ A) where H is Subset of STS(D,d0),
F is Subset of STS(D,d0) : H in T & F in T}
by A3,TMAP_1:def 7;
now let W be set;
assume W in G;
then consider P being Subset of D such that
A7: W = P and A8: d0 in P and P <> D;
reconsider F=D as Subset of D by Lm2;
set H = P \ {d0};
H c= P by XBOOLE_1:36;
then reconsider H as Subset of D by XBOOLE_1:1;
not ex K being Subset of D
st K = F & d0 in K & K <> D;
then not F in G;
then A9: F in T by XBOOLE_0:def 4;
d0 in {d0} by TARSKI:def 1;
then not ex K being Subset of D
st K = H & d0 in K & K <> D by XBOOLE_0:def 4;
then not H in G;
then A10: H in T by XBOOLE_0:def 4;
A c= P & A c= D by A4,A8,ZFMISC_1:37;
then W = H \/ A & A = F /\ A by A4,A7,XBOOLE_1:28,45;
hence W in A-extension_of_the_topology_of STS(D,d0) by A3,A6,A9,A10
;
end;
hence thesis by TARSKI:def 3;
end;
T c= A-extension_of_the_topology_of STS(D,d0) by A3,TMAP_1:99;
then T \/ G c= A-extension_of_the_topology_of STS(D,d0) by A5,XBOOLE_1:8;
then A11: bool D c= A-extension_of_the_topology_of STS(D,d0) by A2,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:104
.= the topology of 1TopSp(D) by A1,A3,A11,XBOOLE_0:def 10;
hence thesis by A1,A3,TMAP_1:104;
end;
begin
:: 5. Discrete and Almost Discrete Spaces.
definition let X be non empty TopSpace;
redefine attr X is discrete means
:Def6: for A being non empty Subset of X holds A is not boundary;
compatibility
proof
hereby assume A1: X is discrete;
let A be non empty Subset of X;
assume A is boundary;
then Int A <> A by TOPS_1:84;
then A is not open by TOPS_1:55;
hence contradiction by A1,TDLAT_3:17;
end;
assume A2: for A being non empty Subset of X holds A is not boundary;
now let A be Subset of X, x be Point of X;
assume A3: A = {x};
hereby per cases;
suppose A = {};
then A = {}X;
hence A is open;
suppose A <> {};
then A is not boundary by A2;
then Int A <> {} & Int A c= {x} by A3,TOPS_1:44,84;
hence A is open by A3,ZFMISC_1:39;
end;
end;
hence X is discrete by TDLAT_3:19;
end;
end;
theorem
X is discrete iff
for A being Subset of X
holds A <> the carrier of X implies A is not dense
proof
hereby assume A1: X is discrete;
assume not for A being Subset of X holds
A <> the carrier of X implies A is not dense;
then consider A being Subset of X such that
A2: A <> the carrier of X and A3: A is dense;
now
reconsider B = A` as non empty Subset of X by A2,TOPS_3:2;
take B;
thus B is boundary by A3,TOPS_3:18;
end;
hence contradiction by A1,Def6;
end;
assume A4: for C being Subset of X holds
C <> the carrier of X implies C is not dense;
assume X is non discrete;
then consider A being non empty Subset of X such that
A5: A is boundary by Def6;
now
take B = A`;
thus B <> the carrier of X & B is dense by A5,TOPS_1:def 4,TOPS_3:1;
end;
hence contradiction by A4;
end;
definition
cluster non almost_discrete ->
non discrete non anti-discrete (non empty TopSpace);
coherence
proof let Y be non empty TopSpace;
assume A1: Y is non almost_discrete;
A2: now assume Y is discrete;
then reconsider Y as discrete TopSpace;
Y is almost_discrete;
hence contradiction by A1;
end;
now assume Y is anti-discrete;
then reconsider Y as anti-discrete TopSpace;
Y is almost_discrete;
hence contradiction by A1;
end;
hence thesis by A2;
end;
end;
definition let X be non empty TopSpace;
redefine attr X is almost_discrete means
:Def7: for A being non empty Subset of X holds A is not nowhere_dense;
compatibility
proof
hereby assume A1: X is almost_discrete;
let A be non empty Subset of X;
Cl A is open by A1,TDLAT_3:24;
then Cl A = Int Cl A by TOPS_1:55;
then A c= Int Cl A & A <> {} by PRE_TOPC:48;
then Int Cl A <> {} by XBOOLE_1:3;
hence A is not nowhere_dense by TOPS_3:def 3;
end;
assume A2: for A being non empty Subset of X holds A is not nowhere_dense;
now let A be Subset of X, x be Point of X;
reconsider B = A as Subset of X;
assume A3: A = {x};
hereby per cases;
suppose A = {};
then Cl A = {}X by PRE_TOPC:52;
hence Cl A is open;
suppose A <> {};
then B is not nowhere_dense by A2;
then Int Cl A <> {} by TOPS_3:def 3;
then A meets Int Cl A by TOPS_3:7;
then A = A /\ Int Cl A by A3,ZFMISC_1:58;
then A c= Int Cl A by XBOOLE_1:17;
then Cl A c= Cl Int Cl A &
Cl Int Cl A c= Cl A by PRE_TOPC:49,TDLAT_1:3;
then Cl A = Cl Int Cl A by XBOOLE_0:def 10;
then Cl A is closed_condensed by TOPS_1:def 7;
then Cl A is condensed by TOPS_1:106;
then A4: Int(Fr(Cl A)) = {} by TOPS_1:110;
now assume Fr(Cl A) <> {};
then Fr(Cl A) is not nowhere_dense by A2;
then A5: Int Cl(Fr(Cl A)) <> {} by TOPS_3:def 3;
Cl (Cl A) /\ Cl ( Cl A)` is closed by TOPS_1:35;
then Fr (Cl A) is closed by TOPS_1:def 2;
hence contradiction by A4,A5,PRE_TOPC:52;
end;
then (Cl A) \ Int Cl A = {} by TOPS_1:77;
then Cl A c= Int Cl A & Int Cl A c= Cl A by TOPS_1:44,XBOOLE_1:37;
hence Cl A is open by XBOOLE_0:def 10;
end;
end;
hence X is almost_discrete by TDLAT_3:27;
end;
end;
theorem Th36:
X is almost_discrete iff
for A being Subset of X holds
A <> the carrier of X implies A is not everywhere_dense
proof
hereby assume A1: X is almost_discrete;
assume not for A being Subset of X holds
A <> the carrier of X implies A is not everywhere_dense;
then consider A being Subset of X such that
A2: A is everywhere_dense and A3: A <> the carrier of X;
now
reconsider B = A` as non empty Subset of X by A3,TOPS_3:2;
take B;
thus B is nowhere_dense by A2,TOPS_3:39;
end;
hence contradiction by A1,Def7;
end;
assume A4: for A being Subset of X holds
A <> the carrier of X implies A is not everywhere_dense;
assume X is non almost_discrete;
then consider A being non empty Subset of X such that
A5: A is nowhere_dense by Def7;
now take B = A`;
thus B <> the carrier of X &
B is everywhere_dense by A5,TOPS_3:1,40;
end;
hence contradiction by A4;
end;
theorem Th37:
X is non almost_discrete iff
ex A being non empty Subset of X st A is boundary & A is closed
proof
thus X is non almost_discrete implies
ex A being non empty Subset of X st A is boundary & A is closed
proof
assume X is non almost_discrete;
then consider A being non empty Subset of X such that
A1: A is nowhere_dense by Def7;
consider C being Subset of X such that
A2: A c= C and A3: C is closed & C is boundary by A1,TOPS_3:27;
reconsider C as non empty Subset of X by A2,XBOOLE_1:3;
reconsider C as non empty Subset of X;
take C;
thus thesis by A3;
end;
given A being non empty Subset of X such that
A4: A is boundary & A is closed;
now
take A;
thus A is nowhere_dense by A4,TOPS_1:93;
end;
hence thesis by Def7;
end;
theorem
X is non almost_discrete iff
ex A being Subset of X st A <> the carrier of X & A is dense & A is open
proof
thus X is non almost_discrete implies
ex A being Subset of X
st A <> the carrier of X & A is dense & A is open
proof
assume X is non almost_discrete;
then consider A being non empty Subset of X such that
A1: A is boundary & A is closed by Th37;
take B = A`;
thus B <> the carrier of X & B is dense & B is open
by A1,TOPS_1:29,def 4,TOPS_3:1;
end;
given A being Subset of X such that
A2: A <> the carrier of X and A3: A is dense & A is open;
now
reconsider B = A` as non empty Subset of X by A2,TOPS_3:2;
take B;
thus B is boundary & B is closed by A3,TOPS_1:30,TOPS_3:18;
end;
hence thesis by Th37;
end;
definition
cluster
almost_discrete non discrete non anti-discrete strict non empty TopSpace;
existence
proof
set C = bool {0,1};
set Y = ADTS(C);
A1: Y = TopStruct(#C,cobool C#) by Def3;
then A2: the topology of Y = {{},C} by Def2;
A3: {} c= {0,1} by XBOOLE_1:2;
then A4: {} in C;
A5: {{}} c= C by A3,ZFMISC_1:37;
reconsider A = {{}} as Subset of Y by A1,A3,ZFMISC_1:37;
set Y1 = Y modified_with_respect_to A;
A6: the carrier of Y1 = the carrier of Y by TMAP_1:104;
then reconsider A1 = A as Subset of Y1;
A7: A1 is open by TMAP_1:105;
now let H be set;
assume H in the topology of Y1;
then H in A-extension_of_the_topology_of Y by TMAP_1:104;
then H in {p \/ (q /\ A) where p,q is Subset of Y :
p in the topology of Y & q in the topology of Y}
by TMAP_1:def 7;
then consider P,Q being Subset of Y such that
A8: H = P \/ (Q /\ A) and
A9: P in the topology of Y & Q in the topology of Y;
now per cases by A2,A9,TARSKI:def 2;
case P = {} & Q = {};
hence H = {} by A8;
case P = C & Q = {};
hence H = C by A8;
case P = {} & Q = C;
hence H = A by A5,A8,XBOOLE_1:28;
case A10: P = C & Q = C;
then Q /\ A = A & C \/ A = C by A5,XBOOLE_1:12,28;
hence H = C by A8,A10;
end;
hence H in {{},A1,C} by ENUMSET1:14;
end;
then A11: the topology of Y1 c= {{},A1,C} by TARSKI:def 3;
set Y2 = Y1 modified_with_respect_to A1`;
take Y2;
A12: the carrier of Y2 = the carrier of Y1 by TMAP_1:104;
then reconsider A2 = A1 as Subset of Y2;
set A3 = A2`;
A13: A2 is closed & A2 is open by A7,Th1,Th3;
then A14: A3 is open by TOPS_1:29;
now let H be set;
assume H in the topology of Y2;
then H in ( A1`)-extension_of_the_topology_of Y1 by TMAP_1:104;
then H in {P \/ (Q /\ A1`) where P,Q is Subset of Y1 :
P in the topology of Y1 & Q in the topology of Y1}
by TMAP_1:def 7;
then consider P,Q being Subset of Y1 such that
A15: H = P \/ (Q /\ A1`) and
A16: P in the topology of Y1 & Q in the topology of Y1;
now per cases by A11,A16,ENUMSET1:13;
case P = {} & Q = {};
hence H = {} by A15;
case P = A1 & Q = {};
hence H = A1 by A15;
case P = C & Q = {};
hence H = C by A15;
case A17: P = {} & Q = A1;
A1 misses A1` by PRE_TOPC:26;
hence H = {} by A15,A17,XBOOLE_0:def 7;
case A18: P = A1 & Q = A1;
A1 misses A1` by PRE_TOPC:26;
then A1 /\ A1` = {}Y1 by XBOOLE_0:def 7;
hence H = A1 by A15,A18;
case A19: P = C & Q = A1;
A1 misses A1` by PRE_TOPC:26;
then A1 /\ A1` = {}Y1 by XBOOLE_0:def 7;
hence H = C by A15,A19;
case A20: P = {} & Q = C;
then Q /\ A1` = A1` by A1,A6,XBOOLE_1:28;
hence H = A2` by A12,A15,A20;
case P = A1 & Q = C;
then H = A1 \/ A1` & A1 \/ A1` = [#]Y1
by A1,A6,A15,PRE_TOPC:18,XBOOLE_1:28;
hence H = C by A1,A6,PRE_TOPC:12;
case P = C & Q = C;
hence H = C by A1,A6,A15,XBOOLE_1:12;
end;
hence H in {{},A2,A3,C} by ENUMSET1:19;
end;
then A21: the topology of Y2 c= {{},A2,A3,C} by TARSKI:def 3;
now let H be set;
assume H in {{},A2,A3,C};
then H = {} or H = A2 or H = A3 or H = C by ENUMSET1:18;
hence H in the topology of Y2 by A1,A6,A12,A13,A14,PRE_TOPC:5,def 1,def
5;
end;
then {{},A2,A3,C} c= the topology of Y2 by TARSKI:def 3;
then A22: the topology of Y2 = {{},A2,A3,C} by A21,XBOOLE_0:def 10;
0 in {0,1} & 1 in {0,1} by TARSKI:def 2;
then reconsider B0 = {0}, B1 = {1} as Subset of {0,1}
by ZFMISC_1:37;
{B0,B1} is non empty Subset of Y2
by A1,A6,A12,ZFMISC_1:38;
then reconsider B = {B0,B1} as non empty Subset of Y2;
A23: now
take A2;
now assume A2 = C;
then B0 = {} by TARSKI:def 1;
hence contradiction;
end;
hence A2 is open & A2 <> {} & A2 <> the carrier of Y2 by A1,A7,A12,Th1,
TMAP_1:104;
end;
A24: now
take B;
Int B in {{},A2,A3,C} by A22,PRE_TOPC:def 5;
then A25: Int B = {} or Int B = A2 or Int B = A3 or Int B = C
by ENUMSET1:18;
A26: now assume Int B = C;
then C c= B by TOPS_1:44;
hence contradiction by A4,TARSKI:def 2;
end;
A27: now assume Int B = A2;
then {} in Int B & Int B c= B by TARSKI:def 1,TOPS_1:44;
hence contradiction by TARSKI:def 2;
end;
now assume A28: Int B = A3;
reconsider I={0,1} as Point of Y2 by A1,A6,A12,ZFMISC_1:def 1;
not I in A2 by TARSKI:def 1;
then I in
Int B & Int B c= B by A28,SUBSET_1:50,TOPS_1:44;
then I = B0 or I = B1 by TARSKI:def 2;
then 1 in B0 or 0 in B1 by TARSKI:def 2;
hence contradiction by TARSKI:def 1;
end;
hence B is boundary by A25,A26,A27,TOPS_1:84;
end;
now let G be Subset of Y2;
assume G is open;
then A29: G in {{},A2,A3,C} by A22,PRE_TOPC:def 5;
A30: now assume G = {} or G = C;
then (G = {}Y2 or G = [#]Y2) & {}Y2 is closed & [#]
Y2 is closed
by A1,A6,A12,PRE_TOPC:12;
hence G is closed;
end;
A31: now assume A32: G = A2;
A3 in the topology of Y2 by A22,ENUMSET1:19;
then A3 is open by PRE_TOPC:def 5;
hence G is closed by A32,TOPS_1:29;
end;
now assume A33: G = A3;
A2 in the topology of Y2 by A22,ENUMSET1:19;
then A2 is open by PRE_TOPC:def 5;
then A3` is open;
hence G is closed by A33,TOPS_1:29;
end;
hence G is closed by A29,A30,A31,ENUMSET1:18;
end;
hence thesis by A23,A24,Def6,TDLAT_3:20,23;
end;
end;
theorem Th39:
for C being non empty set, c0 being Element of C holds
C \ {c0} is non empty iff STS(C,c0) is non almost_discrete
proof let C be non empty set, c0 be Element of C;
A1: STS(C,c0) =
TopStruct(#C,(bool C) \ {A where A is Subset of C : c0 in A & A <> C}#)
by Def5;
hereby assume A2: C \ {c0} is non empty;
now
{c0} is non empty Subset of STS(C,c0)
by A1,ZFMISC_1:37;
then reconsider A = {c0} as non empty Subset of STS(C,c0);
take A;
A is closed & A is boundary by A2,Th25;
hence A is nowhere_dense by TOPS_1:93;
end;
hence STS(C,c0) is non almost_discrete by Def7;
end;
assume STS(C,c0) is non almost_discrete;
then consider A being non empty Subset of STS(C,c0) such that
A3: A is nowhere_dense by Def7;
assume C \ {c0} is empty;
then C c= {c0} & {c0} c= C by XBOOLE_1:37,ZFMISC_1:37;
then C = {c0} by XBOOLE_0:def 10;
then A = C by A1,ZFMISC_1:39;
hence contradiction by A1,A3,TOPS_3:23;
end;
definition
cluster non almost_discrete strict non empty TopSpace;
existence
proof
set D = {0,1};
reconsider a = 0 as Element of D by TARSKI:def 2;
set Y = STS(D,a);
take Y;
Y = TopStruct(#D,(bool D) \ {A where A is Subset of D : a in A & A <> D}
#)
by Def5
;
then reconsider A = {a} as non empty Subset of Y
by ZFMISC_1:37;
1 in D & not 1 in A by TARSKI:def 1,def 2;
then D \ A is non empty by XBOOLE_0:def 4;
hence thesis by Th39;
end;
end;
theorem
for A being non empty Subset of X st A is boundary holds
X modified_with_respect_to A` is non almost_discrete
proof let A be non empty Subset of X;
assume A1: A is boundary;
set Z = X modified_with_respect_to A`;
now
the carrier of X = the carrier of Z &
A c= the carrier of X by TMAP_1:104;
then reconsider C = A as non empty Subset of Z;
take C;
thus C is nowhere_dense by A1,Th7;
end;
hence thesis by Def7;
end;
theorem
for A being Subset of X st A <> the carrier of X & A is dense holds
X modified_with_respect_to A is non almost_discrete
proof let A be Subset of X;
assume A1: A <> the carrier of X;
assume A2: A is dense;
set Z = X modified_with_respect_to A;
now
A is Subset of Z by TMAP_1:104;
then reconsider C = A as Subset of Z;
take C;
thus C <> the carrier of Z &
C is everywhere_dense by A1,A2,Th5,TMAP_1:104;
end;
hence thesis by Th36;
end;