:: On Discrete and Almost Discrete Topological Spaces
:: by Zbigniew Karno
::
:: Received April 6, 1993
:: Copyright (c) 1993-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, PRE_TOPC, SUBSET_1, TMAP_1, RCOMP_1, TARSKI, STRUCT_0,
TOPS_1, TOPS_3, ZFMISC_1, SETFAM_1, TDLAT_3, NATTRA_1, COMPTS_1, TEX_1,
CARD_1;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, SETFAM_1, DOMAIN_1, CARD_1,
STRUCT_0, PRE_TOPC, TOPS_1, TMAP_1, TDLAT_3, TOPS_3, COMPTS_1;
constructors SETFAM_1, DOMAIN_1, TOPS_1, COMPTS_1, PCOMPS_1, TDLAT_3, TMAP_1,
TOPS_3;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, TOPS_1, TDLAT_3, TMAP_1,
CARD_1;
requirements BOOLE, SUBSET, NUMERALS;
definitions PRE_TOPC, TDLAT_3, STRUCT_0;
equalities COMPTS_1, SUBSET_1, STRUCT_0, ORDINAL1;
expansions PRE_TOPC, TDLAT_3, STRUCT_0;
theorems TARSKI, SUBSET_1, ZFMISC_1, ENUMSET1, PRE_TOPC, TOPS_1, PCOMPS_1,
TMAP_1, TDLAT_3, TOPS_3, 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;
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;
hence thesis by A1,A2,A3;
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;
A2: the carrier of (X modified_with_respect_to D) = the carrier of X by
TMAP_1:93;
assume B is closed;
then C` is open by A1,A2,Th1;
hence thesis;
end;
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 TMAP_1:93;
then C` is open by TMAP_1:94;
hence thesis;
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;
set A = (Cl C)`;
A in the topology of (X modified_with_respect_to D) by PRE_TOPC:def 2;
then A in D-extension_of_the_topology_of X by TMAP_1:93;
then
A2: 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;
reconsider B = A as Subset of X by TMAP_1:93;
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 by A2;
A5: H c= A by A3,XBOOLE_1:7;
A6: C c= Cl C by PRE_TOPC:18;
then D misses A by A1,SUBSET_1:24;
then (G /\ D) misses A by XBOOLE_1:17,63;
then
A7: (G /\ D) /\ A = {} by XBOOLE_0:def 7;
A = (H \/ (G /\ D)) /\ A by A3
.= (H /\ A) \/ {} by A7,XBOOLE_1:23
.= H /\ A;
then A c= H by XBOOLE_1:17;
then B = H by A5,XBOOLE_0:def 10;
then
A8: B is open by A4;
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;
then
A10: Cl D = [#]X by TOPS_1:def 3;
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 A9,A10,XBOOLE_1:28;
end;
thus thesis by A1,TMAP_1:94;
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;
reconsider E = D as Subset of X modified_with_respect_to D by TMAP_1:93;
assume
A2: D is dense;
then
A3: E is open by Th4;
E is dense by A2,Th4;
hence thesis by A1,A3,TOPS_3:36,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 TMAP_1:93;
assume D is boundary;
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 thesis by A3,TOPS_1: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;
reconsider E = D as Subset of X modified_with_respect_to D` by TMAP_1:93;
assume
A2: D is boundary;
then
A3: E is closed by Th6;
E is boundary by A2,Th6;
hence thesis by A1,A3,TOPS_3:26;
end;
Lm1: 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 :: redefines trivial (STRUCT_0, redefinition) → trivial (STRUCT_0, definition)
: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 Lm1;
set d = the 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;
hence a in D by TARSKI:def 1;
end;
then A c= D by SUBSET_1:2;
hence thesis 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 by A2,TARSKI:def 1;
hence a = b by A2,TARSKI:def 1;
end;
hence thesis;
end;
end;
registration
cluster 1-element strict for TopStruct;
existence
proof
set O = the 1-element 1-sorted;
reconsider tau = {} as Subset-Family of O by XBOOLE_1:2;
reconsider tau as Subset-Family of O;
take TopStruct (#the carrier of O,tau#);
thus the carrier of TopStruct (#the carrier of O,tau#) is 1-element;
thus thesis;
end;
cluster non trivial strict for TopStruct;
existence
proof
set O =the non trivial 1-sorted;
reconsider tau = {} as Subset-Family of O by XBOOLE_1:2;
take TopStruct (#the carrier of O,tau#);
thus thesis;
end;
end;
theorem
for Y being 1-element TopStruct st the topology of Y is non
empty holds Y is almost_discrete implies Y is TopSpace-like
proof
let Y be 1-element TopStruct;
consider d being Element of Y such that
A1: the carrier of Y = {d} by Def1;
reconsider D = {d} as Subset of Y;
assume the topology of Y is non empty;
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;
A4: bool D = {{},D} by ZFMISC_1:24;
now
per cases by A1,A4,TARSKI:def 2;
suppose
A5: A = {};
D \ A in the topology of Y by A1,A2,A3;
hence {{},D} c= the topology of Y by A2,A5,ZFMISC_1:32;
end;
suppose
A6: A = D;
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;
end;
end;
then the topology of Y = {{}, the carrier of Y} by A1,A4,XBOOLE_0:def 10;
then reconsider Y as anti-discrete TopStruct by TDLAT_3:def 2;
Y is TopSpace-like;
hence thesis;
end;
registration
cluster 1-element strict for TopSpace;
existence
proof
set O =the 1-element 1-sorted;
reconsider tau = bool the carrier of O as Subset-Family of O;
set Y = TopStruct (#the carrier of O,tau#);
reconsider Y as discrete non empty TopStruct by TDLAT_3:def 1;
reconsider Y as TopSpace-like non empty TopStruct;
take Y;
thus the carrier of Y is 1-element;
thus thesis;
end;
end;
registration
cluster -> anti-discrete discrete for 1-element TopSpace;
coherence
proof
let Y be 1-element TopSpace;
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 thesis by A2;
end;
cluster discrete anti-discrete -> trivial for non empty TopSpace;
coherence
proof
let Y be non empty TopSpace;
assume Y is discrete anti-discrete;
then
A3: bool the carrier of Y = {{}, the carrier of Y};
now
set d0 = the Element of Y;
take d0;
thus {d0} = the carrier of Y by A3,TARSKI:def 2;
end;
hence thesis;
end;
end;
registration
cluster non trivial strict for TopSpace;
existence
proof
set D = {{},1};
reconsider tau = bool D as Subset-Family of 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};
d = {} by A1,ZFMISC_1:4;
hence contradiction by A1,ZFMISC_1:4;
end;
hence thesis;
end;
end;
registration
cluster non discrete -> non trivial for non empty TopSpace;
coherence;
cluster non anti-discrete -> non trivial for non empty TopSpace;
coherence;
end;
begin
:: 3. Examples of Discrete and Anti-discrete Topological Spaces.
definition
let D be set;
func cobool D -> Subset-Family of D equals
{{},D};
coherence
proof
A1: D in bool D by ZFMISC_1:def 1;
{} c= D by XBOOLE_1:2;
hence thesis by A1,ZFMISC_1:32;
end;
end;
registration
let D be set;
cluster cobool D -> non empty;
coherence;
end;
definition
let D be set;
func ADTS(D) -> TopStruct equals
TopStruct(#D,cobool D#);
coherence;
end;
registration
let D be set;
cluster ADTS(D) -> strict anti-discrete TopSpace-like;
coherence
proof
set Y = TopStruct (#D,cobool D#);
reconsider Y9 = Y as anti-discrete TopStruct by TDLAT_3:def 2;
Y9 is anti-discrete strict TopSpace;
hence thesis;
end;
end;
registration
let D be non empty set;
cluster ADTS(D) -> non empty;
coherence;
end;
theorem Th9:
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)
by PCOMPS_1:2,TDLAT_3:19;
theorem Th10:
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 by TOPS_1:16;
hence contradiction by A1,XBOOLE_0:def 10;
end;
hence thesis by TDLAT_3:18;
end;
thus A = the carrier of X implies Int A = the carrier of X
proof
assume A = the carrier of X;
then A = [#]X;
hence thesis by TOPS_1:15;
end;
end;
theorem Th11:
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 by PRE_TOPC:22;
hence A = {} or A = the carrier of X by A1;
end;
hence thesis by TDLAT_3:19;
end;
theorem Th12:
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:23;
hence A = {} or A = the carrier of X by A1;
end;
hence thesis by TDLAT_3:18;
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 Th9;
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 Th10;
hence thesis by TOPS_1:48;
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);
for A being Subset of X st A is non empty holds Cl A = the carrier of X
by A1,TOPS_3:def 2;
hence thesis by Th11;
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 = {};
end;
hence thesis by Th12;
end;
registration
let D be set;
cluster 1TopSp D -> discrete;
coherence;
end;
theorem
for X being discrete non empty TopSpace for A being Subset of X holds
Cl A = A & Int A = A
by TDLAT_3:16,TDLAT_3:15,PRE_TOPC:22,TOPS_1:23;
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:16;
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:15;
end;
theorem Th19:
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;
thus ADTS(D) = 1TopSp(D) implies ex d0 being Element of D st D = {d0}
proof
set d0 = the Element of D;
assume
A1: ADTS(D) = 1TopSp(D);
take d0;
thus thesis by A1,TARSKI:def 2;
end;
given d0 being Element of D such that
A2: D = {d0};
thus thesis by A2,ZFMISC_1:24;
end;
registration
cluster discrete non anti-discrete strict non empty for TopSpace;
existence
proof
set D = {{},1};
set Y = 1TopSp(D);
take Y;
now
assume Y is anti-discrete;
then the TopStruct of Y = the TopStruct of ADTS(D);
then consider d0 being Element of D such that
A1: D = {d0} by Th19;
d0 = {} by A1,ZFMISC_1:4;
hence contradiction by A1,ZFMISC_1:4;
end;
hence thesis;
end;
cluster anti-discrete non discrete strict non empty for TopSpace;
existence
proof
set D = {{},1};
set Y = ADTS(D);
take Y;
now
assume Y is discrete;
then the TopStruct of Y = the TopStruct of 1TopSp(D);
then consider d0 being Element of D such that
A2: D = {d0} by Th19;
d0 = {} by A2,ZFMISC_1:4;
hence contradiction by A2,ZFMISC_1:4;
end;
hence thesis;
end;
end;
begin
:: 4. An Example of a Topological Space.
definition
let D be set, d0 be Element of D;
func STS(D,d0) -> TopStruct equals
TopStruct (#D,(bool D) \ {A where A is
Subset of D : d0 in A & A <> D}#);
coherence;
end;
registration
let D be set, d0 be Element of D;
cluster STS(D,d0) -> strict TopSpace-like;
coherence
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) \ G;
set Y = TopStruct (#D,T#);
thus STS(D,d0) is strict;
not ex A being Subset of D st A = E & d0 in A & A <> D;
then
A1: not E in G;
A2: now
let F be Subset-Family of Y;
assume F c= the topology of Y;
then F misses G by XBOOLE_1:63,79;
then
A3: F /\ G = {} by XBOOLE_0:def 7;
now
per cases;
case
union F = D;
hence union F in the topology of Y by A1,XBOOLE_0:def 5;
end;
case
A4: union F <> D;
A5: now
let A be Subset of D;
assume
A6: A in F;
assume A = D;
then D c= union F by A6,ZFMISC_1:74;
hence contradiction by A4,XBOOLE_0:def 10;
end;
now
let A be set;
assume
A7: A in F;
then reconsider B = A as Subset of D;
not B in G by A3,A7,XBOOLE_0:def 4;
then not (d0 in B & B <> D);
hence not d0 in A by A5,A7;
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 5;
end;
end;
hence union F in the topology of Y;
end;
A8: now
let C,E be Subset of Y;
assume that
A9: C in the topology of Y and
A10: E in the topology of Y;
A11: now
let P be Subset of D;
assume that
A12: P in the topology of Y and
A13: P <> D;
not P in G by A12,XBOOLE_0:def 5;
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 A1,XBOOLE_0:def 5;
end;
case
A14: C <> D or E <> D;
now
per cases by A14;
case
A15: C <> D;
C /\ E c= C by XBOOLE_1:17;
then
not ex A being Subset of D st A = C /\ E & d0 in A & A <> D
by A9,A11,A15;
then not C /\ E in G;
hence C /\ E in the topology of Y by XBOOLE_0:def 5;
end;
case
A16: E <> D;
C /\ E c= E by XBOOLE_1:17;
then
not ex A being Subset of D st A = C /\ E & d0 in A & A <> D
by A10,A11,A16;
then not C /\ E in G;
hence C /\ E in the topology of Y by XBOOLE_0:def 5;
end;
end;
hence C /\ E in the topology of Y;
end;
end;
hence C /\ E in the topology of Y;
end;
the carrier of Y in the topology of Y by A1,XBOOLE_0:def 5;
hence thesis by A2,A8;
end;
end;
registration
let D be non empty set, d0 be Element of D;
cluster STS(D,d0) -> non empty;
coherence;
end;
reserve D for non empty set,
d0 for Element of D;
theorem Th20:
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};
thus {d0} c= A implies A is closed
proof
A1: d0 in {d0} by TARSKI:def 1;
assume {d0} c= A;
then not ex Q being Subset of D st Q = Z & d0 in Q & Q <> D by A1,
XBOOLE_0:def 5;
then not Z in G;
then Z in the topology of STS(D,d0) by XBOOLE_0:def 5;
then Z is open;
hence thesis;
end;
assume A is non empty;
then
A2: Z <> D by TOPS_3:1;
assume A is closed;
then Z in the topology of STS(D,d0) by PRE_TOPC:def 2;
then not Z in G by XBOOLE_0:def 5;
then not d0 in Z by A2;
then d0 in A by SUBSET_1:29;
hence thesis by ZFMISC_1:31;
end;
theorem Th21:
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;
set G = {P where P is Subset of D : d0 in P & P <> D};
let A be Subset of STS(D,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
proof
assume
A3: A = {d0};
hence A is closed by Th20;
A4: now
assume
A5: Int A = A;
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 G by A6;
hence contradiction by A2,XBOOLE_0:def 5;
end;
Int A c= A by TOPS_1:16;
then Int A = {} or Int A = A by A3,ZFMISC_1:33;
hence thesis by A4,TOPS_1:48;
end;
thus A is non empty & A is closed & A is boundary implies A = {d0}
proof
set Z = A \ {d0};
assume that
A7: A is non empty and
A8: A is closed;
A9: {d0} c= A by A7,A8,Th20;
A10: Z c= A by XBOOLE_1:36;
reconsider Z as Subset of STS(D,d0);
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 5;
then not Z in G;
then Z in the topology of STS(D,d0) by XBOOLE_0:def 5;
then
A11: Z is open;
assume A is boundary;
then
A12: Int A = {};
assume
A13: A <> {d0};
now
assume Z = {};
then A c= {d0} by XBOOLE_1:37;
hence contradiction by A9,A13,XBOOLE_0:def 10;
end;
hence contradiction by A10,A12,A11,TOPS_1:24,XBOOLE_1:3;
end;
end;
theorem Th22:
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`;
reconsider P = {d0} as Subset of STS(D,d0);
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 P c= Z by PRE_TOPC:3;
then Z is closed by Th20;
hence thesis by TOPS_1:4;
end;
thus A <> D & A is open implies A c= D \ {d0}
proof
assume A <> D;
then
A1: Z <> {}STS(D,d0) by TOPS_3:2;
assume A is open;
then {d0} c= Z by A1,Th20;
then Z` c= P` by SUBSET_1:12;
hence thesis;
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;
reconsider P = {d0} as Subset of STS(D,d0);
let A be Subset of STS(D,d0);
set Z = A`;
thus A = D \ {d0} implies A is open & A is dense
proof
assume
A2: A = D \ {d0};
hence A is open by Th22;
[#]STS(D,d0) \ ([#]STS(D,d0) \ P) = Z by A2;
then P = Z by PRE_TOPC:3;
then Z is boundary by A1,Th21;
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
A3: Z <> {}STS(D,d0) by TOPS_3:2;
assume
A4: A is open;
assume A is dense;
then Z is boundary by TOPS_3:18;
then Z = {d0} by A1,A3,A4,Th21;
then A = P`;
hence thesis;
end;
end;
registration
cluster non anti-discrete non discrete strict non empty for TopSpace;
existence
proof
set D = {{},1};
reconsider a = {} as Element of D by TARSKI:def 2;
set Y = STS(D,a);
take Y;
reconsider A = {a} as non empty Subset of Y;
A1: not 1 in A by TARSKI:def 1;
1 in D by TARSKI:def 2;
then
A2: D \ A is non empty by A1,XBOOLE_0:def 5;
then A is boundary by Th21;
then Int A <> A;
then
A3: A is not open by TOPS_1:23;
A is closed by A2,Th21;
hence thesis by A3,TDLAT_3:19;
end;
end;
theorem Th24:
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;
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) by TOPS_3:79,Th20;
assume
A1: the carrier of Y = D;
assume
A2: 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
A3: A = C;
A4: now
assume
A5: C is closed;
now
per cases;
case
C = {};
hence A is closed by A3;
end;
case
C <> {};
then {d0} c= A by A3,A5,Th20;
hence A is closed by A2;
end;
end;
hence A is closed;
end;
now
assume
A6: A is closed;
now
per cases;
case
A = {};
hence C is closed by A3;
end;
case
A <> {};
then {d0} c= C by A2,A3,A6;
hence C is closed by Th20;
end;
end;
hence C is closed;
end;
hence A is closed iff C is closed by A4;
end;
hence thesis by A1,TOPS_3:73;
end;
theorem Th25:
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;
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})
by Th22,TOPS_3:76;
assume
A1: the carrier of Y = D;
assume
A2: 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
A3: A = C;
A4: now
assume
A5: A is open;
now
per cases;
case
A = D;
then C = [#]STS(D,d0) by A3;
hence C is open;
end;
case
A <> D;
then A c= D \ {d0} by A2,A5;
hence C is open by A3,Th22;
end;
end;
hence C is open;
end;
now
assume
A6: C is open;
now
per cases;
case
C = D;
then A = [#]Y by A1,A3;
hence A is open;
end;
case
C <> D;
then A c= D \ {d0} by A3,A6,Th22;
hence A is open by A2;
end;
end;
hence A is open;
end;
hence A is open iff C is open by A4;
end;
hence thesis by A1,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;
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
A1: the TopStruct of Y = the TopStruct of STS(D,d0);
hence the carrier of Y = D;
reconsider P = {d0} as Subset of Y by A1;
now
let A be non empty Subset of Y;
reconsider B = A as Subset of Y;
Cl A is non 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;
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 A is non empty;
then
A7: Cl A = A \/ {d0} by A6;
assume A is closed;
then
A8: Cl A = A by PRE_TOPC:22;
assume not {d0} c= A;
hence contradiction by A7,A8,XBOOLE_1:7;
end;
end;
hence thesis by A5,Th24;
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;
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
A1: the TopStruct of Y = the TopStruct of STS(D,d0);
hence the carrier of Y = D;
reconsider P = {d0} as Subset of Y by A1;
now
let A be Subset of Y;
reconsider B = A as Subset of Y;
A2: A = A /\ D by A1,XBOOLE_1:28;
assume
A3: A <> D;
now
assume Int A = D;
then D c= A by TOPS_1:16;
hence contradiction by A1,A3,XBOOLE_0:def 10;
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;
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
D /\ {d0} = {d0} by ZFMISC_1:46;
then
A10: D meets {d0} by XBOOLE_0:def 7;
assume A = D;
then D = D \ {d0} by A8,XBOOLE_0:def 10;
hence contradiction by A10,XBOOLE_1:83;
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 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:23;
then A \ {d0} = A by A7,A12;
hence thesis by A6,XBOOLE_1:33;
end;
end;
hence thesis by A6,Th25;
end;
Lm2: 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};
set x = the Element of G;
assume
A2: D = {d0};
assume G <> {};
then x in G;
then consider S being Subset of D such that
x = S and
A3: d0 in S and
A4: S <> D by A1;
set d1 = the Element of D \ S;
A5: now
assume D \ S = {};
then D c= S by XBOOLE_1:37;
hence contradiction by A4,XBOOLE_0:def 10;
end;
then reconsider d1 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;
end;
theorem
STS(D,d0) = ADTS(D) iff D = {d0}
proof
set G = {P where P is Subset of D : d0 in P & P <> D};
thus STS(D,d0) = ADTS(D) implies D = {d0}
proof
set d1 = the Element of D \ {d0};
assume
A1: STS(D,d0) = ADTS(D);
assume
A2: D <> {d0};
A3: now
assume D \ {d0} = {};
then D c= {d0} by XBOOLE_1:37;
hence contradiction by A2,XBOOLE_0:def 10;
end;
then reconsider d1 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 not ex Q being Subset of D st Q = P & d0 in Q & Q <> D by TARSKI:def 1
;
then not P in G;
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;
end;
assume
A6: D = {d0};
then G = {} by Lm2;
hence thesis by A6,ZFMISC_1:24;
end;
theorem
STS(D,d0) = 1TopSp(D) iff D = {d0}
proof
set G = {P where P is Subset of D : d0 in P & P <> D};
thus STS(D,d0) = 1TopSp(D) implies D = {d0}
proof
now
let x be object;
assume x in G;
then ex Q being Subset of D st x = Q & d0 in Q & Q <> D;
hence x in bool D;
end;
then
A1: G c= bool D by TARSKI:def 3;
reconsider P = {d0} as Subset of D;
assume
A2: STS(D,d0) = 1TopSp(D);
A3: d0 in P by TARSKI:def 1;
assume D <> {d0};
then P in G by A3;
hence contradiction by A2,A1,XBOOLE_1:38;
end;
assume D = {d0};
then G = {} by Lm2;
hence thesis;
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;
set G = {P where P is Subset of D : d0 in P & P <> D};
set T = (bool D) \ G;
let A be Subset of STS(D,d0);
assume
A1: A = {d0};
A2: 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
TMAP_1:def 7;
now
reconsider F=D as Subset of D by Lm1;
let W be object;
assume W in G;
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 as Subset of D;
A c= P by A1,A4,ZFMISC_1:31;
then
A5: W = H \/ A by A1,A3,XBOOLE_1:45;
not ex K being Subset of D st K = F & d0 in K & K <> D;
then not F in G;
then
A6: F in T by XBOOLE_0:def 5;
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 5;
then not H in G;
then
A7: H in T 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;
end;
then
A8: G c= A-extension_of_the_topology_of STS(D,d0) by TARSKI:def 3;
T \/ G = (bool D) \/ G by XBOOLE_1:39;
then
A9: bool D c= T \/ G by XBOOLE_1:7;
T c= A-extension_of_the_topology_of STS(D,d0) by TMAP_1:88;
then T \/ G 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 thesis by TMAP_1:93;
end;
begin
:: 5. Discrete and Almost Discrete Spaces.
definition
let X be non empty TopSpace;
redefine attr X is discrete means :: redefines discrete (TDLAT_3, definition)
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;
then A is not open by TOPS_1:23;
hence contradiction by A1;
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 = {};
hence A is open;
end;
suppose
A <> {};
then A is not 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;
end;
end;
end;
hence thesis by TDLAT_3:17;
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;
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;
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;
registration
cluster non almost_discrete -> non discrete non anti-discrete for non empty
TopSpace;
coherence;
end;
definition
let X be non empty TopSpace;
redefine attr X is almost_discrete means :: redefines almost_discrete (TDLAT_3, definition)
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:22;
then Cl A = Int Cl A by TOPS_1:23;
then Int Cl A <> {} by PRE_TOPC:18,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;
assume A = {x};
hereby
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;
end;
end;
hence thesis by TDLAT_3:25;
end;
end;
theorem Th32:
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;
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;
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 Th33:
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;
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 as non empty Subset of X by A2;
reconsider C as non empty Subset of X;
take C;
thus thesis by A3,A4;
end;
given A being non empty Subset of X such that
A5: A is boundary and
A6: A is closed;
thus thesis by A5,A6;
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 and
A2: A is closed by Th33;
take A`;
thus thesis by A1,A2,TOPS_3:1;
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;
now
reconsider B = A` as non empty Subset of X by A3,TOPS_3:2;
take B;
thus B is boundary & B is closed by A4,A5,TOPS_3:18;
end;
hence thesis;
end;
registration
cluster almost_discrete non discrete non anti-discrete strict non empty
for TopSpace;
existence
proof
set C = bool {{},1};
set Y = ADTS(C);
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 Y by ZFMISC_1:31;
set Y1 = Y modified_with_respect_to A;
A3: the carrier of Y1 = the carrier of Y by TMAP_1:93;
reconsider A1 = A as Subset of Y1 by TMAP_1:93;
set Y2 = Y1 modified_with_respect_to A1`;
reconsider A2 = A1 as Subset of Y2 by TMAP_1:93;
set A3 = A2`;
A4: the carrier of Y2 = the carrier of Y1 by TMAP_1:93;
then reconsider B = {B0,B1} as non empty Subset of Y2 by TMAP_1:93;
now
let H be object;
assume H in the topology of Y1;
then H in A-extension_of_the_topology_of Y by TMAP_1:93;
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
A5: H = P \/ (Q /\ A) and
A6: P in the topology of Y and
A7: Q in the topology of Y;
now
per cases by A6,A7,TARSKI:def 2;
case
P = {} & Q = {};
hence H = {} by A5;
end;
case
P = C & Q = {};
hence H = C by A5;
end;
case
P = {} & Q = C;
hence H = A by A5,XBOOLE_1:28;
end;
case
P = C & Q = C;
hence H = C by A5,XBOOLE_1:12;
end;
end;
hence H in {{},A1,C} by ENUMSET1:def 1;
end;
then
A8: the topology of Y1 c= {{},A1,C} by TARSKI:def 3;
now
let H be object;
assume H in the topology of Y2;
then H in ( A1`)-extension_of_the_topology_of Y1 by TMAP_1:93;
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
A9: H = P \/ (Q /\ A1`) and
A10: P in the topology of Y1 and
A11: Q in the topology of Y1;
now
per cases by A8,A10,A11,ENUMSET1:def 1;
case
P = {} & Q = {};
hence H = {} by A9;
end;
case
P = A1 & Q = {};
hence H = A1 by A9;
end;
case
P = C & Q = {};
hence H = C by A9;
end;
case
A12: P = {} & Q = A1;
A1 misses A1` by XBOOLE_1:79;
hence H = {} by A9,A12,XBOOLE_0:def 7;
end;
case
A13: P = A1 & Q = A1;
A1 misses A1` by XBOOLE_1:79;
then A1 /\ A1` = {}Y1 by XBOOLE_0:def 7;
hence H = A1 by A9,A13;
end;
case
A14: P = C & Q = A1;
A1 misses A1` by XBOOLE_1:79;
then A1 /\ A1` = {}Y1 by XBOOLE_0:def 7;
hence H = C by A9,A14;
end;
case
P = {} & Q = C;
hence H = A2` by A3,A4,A9,XBOOLE_1:28;
end;
case
A15: P = A1 & Q = C;
A1 \/ A1` = [#]Y1 by PRE_TOPC:2;
hence H = C by A3,A9,A15,XBOOLE_1:28;
end;
case
P = C & Q = C;
hence H = C by A3,A9,XBOOLE_1:12;
end;
end;
hence H in {{},A2,A3,C} by ENUMSET1:def 2;
end;
then
A16: the topology of Y2 c= {{},A2,A3,C} by TARSKI:def 3;
A17: A2 is open by Th1,TMAP_1:94;
A18: A2 is closed by Th3;
now
let H be object;
assume H in {{},A2,A3,C};
then H = {} or H = A2 or H = A3 or H = C by ENUMSET1:def 2;
hence H in the topology of Y2 by A3,A4,A18,A17,PRE_TOPC:1,def 2;
end;
then {{},A2,A3,C} c= the topology of Y2 by TARSKI:def 3;
then
A19: the topology of Y2 = {{},A2,A3,C} by A16,XBOOLE_0:def 10;
A20: now
let G be Subset of Y2;
A21: G = {} or G = C implies G is closed by A4,TMAP_1:93;
A22: now
A3 in the topology of Y2 by A19,ENUMSET1:def 2;
then
A23: A3 is open;
assume G = A2;
hence G is closed by A23;
end;
A24: now
A2 in the topology of Y2 by A19,ENUMSET1:def 2;
then
A25: A3` is open;
assume G = A3;
hence G is closed by A25;
end;
assume G is open;
then G in {{},A2,A3,C} by A19;
hence G is closed by A21,A22,A24,ENUMSET1:def 2;
end;
A26: {} in C by A2;
A27: now
A28: now
reconsider I={{},1} as Point of Y2 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 = A3;
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;
end;
take B;
A31: now
assume Int B = A2;
then
A32: {} in Int B by TARSKI:def 1;
Int B c= B by TOPS_1:16;
hence contradiction by A32,TARSKI:def 2;
end;
A33: now
assume Int B = C;
then C c= B by TOPS_1:16;
hence contradiction by A26,TARSKI:def 2;
end;
Int B in {{},A2,A3,C} by A19,PRE_TOPC:def 2;
then Int B = {} or Int B = A2 or Int B = A3 or Int B = C by
ENUMSET1:def 2;
hence B is boundary by A33,A31,A28,TOPS_1:48;
end;
take Y2;
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 A4,Th1,TMAP_1:93
,94;
end;
hence thesis by A27,A20,TDLAT_3:18,21;
end;
end;
theorem Th35:
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;
hereby
assume
A1: C \ {c0} is non empty;
now
reconsider A = {c0} as non empty Subset of STS(C,c0);
take A;
A2: A is boundary by A1,Th21;
A is closed by A1,Th21;
hence A is nowhere_dense by A2;
end;
hence STS(C,c0) is non almost_discrete;
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;
assume C \ {c0} is empty;
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;
end;
registration
cluster non almost_discrete strict non empty for TopSpace;
existence
proof
set D = {{},1};
reconsider a = {} as Element of D by TARSKI:def 2;
set Y = STS(D,a);
take Y;
reconsider A = {a} as non empty Subset of Y;
A1: not 1 in A by TARSKI:def 1;
1 in D by TARSKI:def 2;
then D \ A is non empty by A1,XBOOLE_0:def 5;
hence thesis by Th35;
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;
set Z = X modified_with_respect_to A`;
assume
A1: A is boundary;
now
reconsider C = A as non empty Subset of Z by TMAP_1:93;
take C;
thus C is nowhere_dense by A1,Th7;
end;
hence thesis;
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;
set Z = X modified_with_respect_to A;
assume
A2: A is dense;
now
reconsider C = A as Subset of Z by TMAP_1:93;
take C;
thus C <> the carrier of Z & C is everywhere_dense by A1,A2,Th5,TMAP_1:93;
end;
hence thesis by Th32;
end;