:: On Kolmogorov Topological Spaces
:: by Zbigniew Karno
::
:: Received July 26, 1994
:: Copyright (c) 1994-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 PRE_TOPC, STRUCT_0, TARSKI, SUBSET_1, RCOMP_1, XBOOLE_0,
ZFMISC_1, TDLAT_3, NATTRA_1, SETFAM_1, TSP_1;
notations TARSKI, XBOOLE_0, SUBSET_1, DOMAIN_1, STRUCT_0, PRE_TOPC, BORSUK_1,
TSEP_1, TDLAT_3, TEX_2, TEX_4;
constructors REALSET2, BORSUK_1, TSEP_1, TDLAT_3, TEX_2, TEX_4, T_0TOPSP;
registrations XBOOLE_0, STRUCT_0, TOPS_1, TDLAT_3, TEX_1, TEX_2, SUBSET_1,
ZFMISC_1;
requirements SUBSET, BOOLE;
definitions T_0TOPSP;
equalities SUBSET_1, STRUCT_0;
expansions T_0TOPSP, SUBSET_1;
theorems ZFMISC_1, SUBSET_1, PRE_TOPC, TOPS_1, TSEP_1, TDLAT_3, TEX_1, TEX_2,
TEX_4, TARSKI, STRUCT_0, XBOOLE_0, XBOOLE_1;
begin
:: 1. Subspaces.
definition
let Y be TopStruct;
redefine mode SubSpace of Y means :: redefines SubSpace (PRE_TOPC, definition)
:Def1:
the carrier of it c= the carrier of Y &
for G0 being Subset of it holds G0 is open iff ex G being
Subset of Y st G is open & G0 = G /\ the carrier of it;
compatibility
proof
let Y0 be TopStruct;
A1: [#]Y0 = the carrier of Y0 & [#]Y = the carrier of Y;
thus Y0 is SubSpace of Y implies the carrier of Y0 c= the carrier of Y &
for G0 being Subset of Y0 holds G0 is open iff ex G being Subset of Y st G is
open & G0 = G /\ the carrier of Y0
proof
assume
A2: Y0 is SubSpace of Y;
hence the carrier of Y0 c= the carrier of Y by A1,PRE_TOPC:def 4;
thus for G0 being Subset of Y0 holds G0 is open iff ex G being Subset of
Y st G is open & G0 = G /\ the carrier of Y0
proof
let G0 be Subset of Y0;
thus G0 is open implies ex G being Subset of Y st G is open & G0 = G
/\ the carrier of Y0
proof
assume G0 is open;
then G0 in the topology of Y0 by PRE_TOPC:def 2;
then consider G being Subset of Y such that
A3: G in the topology of Y and
A4: G0 = G /\ [#] Y0 by A2,PRE_TOPC:def 4;
reconsider G as Subset of Y;
take G;
thus G is open by A3,PRE_TOPC:def 2;
thus thesis by A4;
end;
given G being Subset of Y such that
A5: G is open and
A6: G0 = G /\ the carrier of Y0;
G in the topology of Y & G0 = G /\ [#]Y0 by A6,A5,PRE_TOPC:def 2;
then G0 in the topology of Y0 by A2,PRE_TOPC:def 4;
hence thesis by PRE_TOPC:def 2;
end;
end;
assume that
A7: the carrier of Y0 c= the carrier of Y and
A8: for G0 being Subset of Y0 holds G0 is open iff ex G being Subset
of Y st G is open & G0 = G /\ the carrier of Y0;
A9: for G0 being Subset of Y0 holds G0 in the topology of Y0 iff ex G
being Subset of Y st G in the topology of Y & G0 = G /\ [#]Y0
proof
let G0 be Subset of Y0;
reconsider M = G0 as Subset of Y0;
thus G0 in the topology of Y0 implies ex G being Subset of Y st G in the
topology of Y & G0 = G /\ [#]Y0
proof
reconsider M = G0 as Subset of Y0;
assume G0 in the topology of Y0;
then M is open by PRE_TOPC:def 2;
then consider G being Subset of Y such that
A10: G is open and
A11: G0 = G /\ the carrier of Y0 by A8;
take G;
thus G in the topology of Y by A10,PRE_TOPC:def 2;
thus thesis by A11;
end;
given G being Subset of Y such that
A12: G in the topology of Y and
A13: G0 = G /\ [#]Y0;
reconsider G as Subset of Y;
G is open & G0 = G /\ the carrier of Y0 by A13,A12,PRE_TOPC:def 2;
then M is open by A8;
hence thesis by PRE_TOPC:def 2;
end;
[#]Y0 c= [#]Y by A7;
hence thesis by A9,PRE_TOPC:def 4;
end;
end;
theorem Th1:
for Y being TopStruct, Y0 being SubSpace of Y for G being Subset
of Y st G is open holds ex G0 being Subset of Y0 st G0 is open & G0 = G /\ the
carrier of Y0
proof
let Y be TopStruct, Y0 be SubSpace of Y;
let G be Subset of Y;
assume
A1: G is open;
[#]Y0 = the carrier of Y0 & [#]Y = the carrier of Y;
then reconsider A = the carrier of Y0 as Subset of Y by PRE_TOPC:def 4;
reconsider G0 = G /\ A as Subset of Y0 by XBOOLE_1:17;
take G0;
thus G0 is open by A1,Def1;
thus thesis;
end;
definition
let Y be TopStruct;
redefine mode SubSpace of Y means :: redefines SubSpace (TSP_1, redefinition) → SubSpace (PRE_TOPC, definition)
:Def2:
the carrier of it c= the carrier of Y &
for F0 being Subset of it holds F0 is closed iff ex F being
Subset of Y st F is closed & F0 = F /\ the carrier of it;
compatibility
proof
let Y0 be TopStruct;
A1: [#]Y0 = the carrier of Y0 & [#]Y = the carrier of Y;
thus Y0 is SubSpace of Y implies the carrier of Y0 c= the carrier of Y &
for F0 being Subset of Y0 holds F0 is closed iff ex F being Subset of Y st F is
closed & F0 = F /\ the carrier of Y0
proof
assume
A2: Y0 is SubSpace of Y;
hence the carrier of Y0 c= the carrier of Y by A1,PRE_TOPC:def 4;
[#]Y0 c= [#]Y by A2,PRE_TOPC:def 4;
then
A3: [#]Y0 \ [#]Y = {} by XBOOLE_1:37;
thus for F0 being Subset of Y0 holds F0 is closed iff ex F being Subset
of Y st F is closed & F0 = F /\ the carrier of Y0
proof
let F0 be Subset of Y0;
set G0 = [#]Y0 \F0;
thus F0 is closed implies ex F being Subset of Y st F is closed & F0 =
F /\ the carrier of Y0
proof
assume F0 is closed;
then [#]Y0 \ F0 is open by PRE_TOPC:def 3;
then consider G being Subset of Y such that
A4: G is open and
A5: [#]Y0 \ F0 = G /\ the carrier of Y0 by A2,Def1;
take F = [#]Y \ G;
A6: G = [#]Y \ F by PRE_TOPC:3;
hence F is closed by A4,PRE_TOPC:def 3;
F0 = [#]Y0 \ (G /\ the carrier of Y0) by A5,PRE_TOPC:3
.= ([#]Y0 \ G) \/ ([#]Y0 \ the carrier of Y0) by XBOOLE_1:54
.= ([#]Y0 \ G) \/ {} by XBOOLE_1:37
.= ([#]Y0 \ [#]Y) \/ ([#]Y0 /\ F) by A6,XBOOLE_1:52
.= [#]Y0 /\ F by A3;
hence thesis;
end;
given F being Subset of Y such that
A7: F is closed and
A8: F0 = F /\ the carrier of Y0;
now
take G = [#]Y \ F;
A9: F = [#]Y \ G by PRE_TOPC:3;
thus G is open by A7,PRE_TOPC:def 3;
G0 = ([#]Y0 \ F) \/ ([#]Y0 \ the carrier of Y0) by A8,XBOOLE_1:54
.= ([#]Y0 \ F) \/ {} by XBOOLE_1:37
.= ([#]Y0 \ [#]Y) \/ ([#]Y0 /\ G) by A9,XBOOLE_1:52
.= [#]Y0 /\ G by A3;
hence G0 = G /\ the carrier of Y0;
end;
then G0 is open by A2,Def1;
hence thesis by PRE_TOPC:def 3;
end;
end;
assume that
A10: the carrier of Y0 c= the carrier of Y and
A11: for F0 being Subset of Y0 holds F0 is closed iff ex F being
Subset of Y st F is closed & F0 = F /\ the carrier of Y0;
A12: [#]Y0 \ [#]Y = {} by A10,XBOOLE_1:37;
for G0 being Subset of Y0 holds G0 is open iff ex G being Subset of Y
st G is open & G0 = G /\ the carrier of Y0
proof
let G0 be Subset of Y0;
set F0 = [#]Y0 \ G0;
thus G0 is open implies ex G being Subset of Y st G is open & G0 = G /\
the carrier of Y0
proof
set F0 = [#]Y0 \ G0;
A13: G0 = [#]Y0 \ F0 by PRE_TOPC:3;
assume G0 is open;
then F0 is closed by A13,PRE_TOPC:def 3;
then consider F being Subset of Y such that
A14: F is closed and
A15: F0 = F /\ the carrier of Y0 by A11;
take G = [#]Y \ F;
thus G is open by A14,PRE_TOPC:def 3;
A16: F = [#]Y \ G by PRE_TOPC:3;
G0 = ([#]Y0 \ F) \/ ([#]Y0 \ the carrier of Y0) by A13,A15,XBOOLE_1:54
.= ([#]Y0 \ F) \/ {} by XBOOLE_1:37
.= ([#]Y0 \ [#]Y) \/ ([#]Y0 /\ G) by A16,XBOOLE_1:52
.= [#]Y0 /\ G by A12;
hence thesis;
end;
given G being Subset of Y such that
A17: G is open and
A18: G0 = G /\ the carrier of Y0;
now
take F = [#]Y \ G;
A19: G = [#]Y \ F by PRE_TOPC:3;
hence F is closed by A17,PRE_TOPC:def 3;
F0 = ([#]Y0 \ G) \/ ([#]Y0 \ the carrier of Y0) by A18,XBOOLE_1:54
.= ([#]Y0 \ G) \/ {} by XBOOLE_1:37
.= ([#]Y0 \ [#]Y) \/ ([#]Y0 /\ F) by A19,XBOOLE_1:52
.= [#]Y0 /\ F by A12;
hence F0 = F /\ the carrier of Y0;
end;
then G0 = [#]Y0 \ F0 & F0 is closed by A11,PRE_TOPC:3;
hence thesis by PRE_TOPC:def 3;
end;
hence Y0 is SubSpace of Y by A10,Def1;
end;
end;
theorem Th2:
for Y being TopStruct, Y0 being SubSpace of Y for F being Subset
of Y st F is closed holds ex F0 being Subset of Y0 st F0 is closed & F0 = F /\
the carrier of Y0
proof
let Y be TopStruct, Y0 be SubSpace of Y;
let F be Subset of Y;
assume
A1: F is closed;
[#]Y0 = the carrier of Y0 & [#]Y = the carrier of Y;
then reconsider A = the carrier of Y0 as Subset of Y by PRE_TOPC:def 4;
reconsider F0 = F /\ A as Subset of Y0 by XBOOLE_1:17;
take F0;
thus F0 is closed by A1,Def2;
thus thesis;
end;
begin
:: 2. Kolmogorov Spaces.
definition
let T be TopStruct;
redefine attr T is T_0 means :: redefines T_0 (PRE_TOPC, definition)
T is empty or for x, y being Point of T
st x <> y holds (ex V being Subset of T st V is open & x in V & not y in V) or
ex W being Subset of T st W is open & not x in W & y in W;
compatibility
proof
hereby
assume
A1: T is T_0;
assume
A2: T is not empty;
let x, y be Point of T;
assume x <> y;
then
ex V being Subset of T st V is open & ( x in V & not y in V or y in
V & not x in V ) by A1,A2;
hence
(ex V being Subset of T st V is open & x in V & not y in V) or ex W
being Subset of T st W is open & not x in W & y in W;
end;
assume
A3: T is empty or for x, y being Point of T st x <> y holds (ex V
being Subset of T st V is open & x in V & not y in V) or ex W being Subset of T
st W is open & not x in W & y in W;
assume
A4: T is not empty;
let x,y be Point of T;
assume x <> y;
then (ex V being Subset of T st V is open & x in V & not y in V) or ex W
being Subset of T st W is open & not x in W & y in W by A3,A4;
hence thesis;
end;
end;
definition
let Y be TopStruct;
redefine attr Y is T_0 means :: redefines T_0 (TSP_1, redefinition) → T_0 (PRE_TOPC, definition)
Y is empty or for x, y being Point of Y
st x <> y holds (ex E being Subset of Y st E is closed & x in E & not y in E)
or ex F being Subset of Y st F is closed & not x in F & y in F;
compatibility
proof
thus Y is T_0 implies Y is empty or for x, y being Point of Y st x <> y
holds (ex E being Subset of Y st E is closed & x in E & not y in E) or ex F
being Subset of Y st F is closed & not x in F & y in F
proof
assume
A1: Y is empty or for x, y being Point of Y st x <> y holds (ex V
being Subset of Y st V is open & x in V & not y in V) or ex W being Subset of Y
st W is open & not x in W & y in W;
assume
A2: Y is not empty;
let x, y be Point of Y;
assume
A3: x <> y;
hereby
per cases by A1,A2,A3;
suppose
ex V being Subset of Y st V is open & x in V & not y in V;
then consider V being Subset of Y such that
A4: V is open and
A5: x in V and
A6: not y in V;
now
take F = V`;
V = [#]Y \ F by PRE_TOPC:3;
hence F is closed by A4,PRE_TOPC:def 3;
thus not x in F by A5,XBOOLE_0:def 5;
thus y in F by A2,A6,SUBSET_1:29;
end;
hence thesis;
end;
suppose
ex W being Subset of Y st W is open & not x in W & y in W;
then consider W being Subset of Y such that
A7: W is open and
A8: not x in W and
A9: y in W;
now
take E = W`;
W = [#]Y \ E by PRE_TOPC:3;
hence E is closed by A7,PRE_TOPC:def 3;
thus x in E by A2,A8,SUBSET_1:29;
thus not y in E by A9,XBOOLE_0:def 5;
end;
hence thesis;
end;
end;
end;
assume
A10: Y is empty or for x, y being Point of Y st x <> y holds (ex E
being Subset of Y st E is closed & x in E & not y in E) or ex F being Subset of
Y st F is closed & not x in F & y in F;
Y is not empty implies for x, y being Point of Y st x <> y holds (ex
V being Subset of Y st V is open & x in V & not y in V) or ex W being Subset of
Y st W is open & not x in W & y in W
proof
assume
A11: Y is not empty;
let x, y be Point of Y;
assume
A12: x <> y;
hereby
per cases by A10,A11,A12;
suppose
ex E being Subset of Y st E is closed & x in E & not y in E;
then consider E being Subset of Y such that
A13: E is closed and
A14: x in E and
A15: not y in E;
now
take W = E`;
W = [#]Y \ E;
hence W is open by A13,PRE_TOPC:def 3;
thus not x in W by A14,XBOOLE_0:def 5;
thus y in W by A11,A15,SUBSET_1:29;
end;
hence thesis;
end;
suppose
ex F being Subset of Y st F is closed & not x in F & y in F;
then consider F being Subset of Y such that
A16: F is closed and
A17: not x in F and
A18: y in F;
now
take V = F`;
V = [#]Y \ F;
hence V is open by A16,PRE_TOPC:def 3;
thus x in V by A11,A17,SUBSET_1:29;
thus not y in V by A18,XBOOLE_0:def 5;
end;
hence thesis;
end;
end;
end;
hence thesis;
end;
end;
registration
cluster trivial -> T_0 for non empty TopStruct;
coherence
proof
let Y be non empty TopStruct;
assume Y is trivial;
then consider a being Point of Y such that
A1: the carrier of Y = {a} by TEX_1:def 1;
now
let x, y be Point of Y;
assume
A2: x <> y;
x = a by A1,TARSKI:def 1;
hence
(ex V being Subset of Y st V is open & x in V & not y in V) or ex W
being Subset of Y st W is open & not x in W & y in W by A1,A2,TARSKI:def 1;
end;
hence thesis;
end;
end;
Lm1: for X being anti-discrete non trivial TopStruct holds X is
non T_0
proof
let X be anti-discrete non trivial TopStruct;
now
consider x, y being Point of X such that
A1: x <> y by STRUCT_0:def 10;
take x, y;
thus x <> y by A1;
A2: now
let V be Subset of X;
assume V is open;
then
A3: V = {} or V = the carrier of X by TDLAT_3:18;
assume y in V;
hence x in V by A3;
end;
now
let V be Subset of X;
assume V is open;
then
A4: V = {} or V = the carrier of X by TDLAT_3:18;
assume x in V;
hence y in V by A4;
end;
hence
not (ex V being Subset of X st V is open & x in V & not y in V) & not
(ex W being Subset of X st W is open & not x in W & y in W) by A2;
end;
hence thesis;
end;
registration
cluster strict T_0 non empty for TopSpace;
existence
proof
set X = the trivial strict non empty TopSpace;
take X;
thus thesis;
end;
cluster strict non T_0 non empty for TopSpace;
existence
proof
set X = the anti-discrete non trivial strict non empty TopSpace;
take X;
thus thesis by Lm1;
end;
end;
registration
cluster discrete -> T_0 for non empty TopSpace;
coherence
proof
let Y be non empty TopSpace;
assume
A1: Y is discrete;
now
let x, y be Point of Y;
assume
A2: x <> y;
now
take V = {x};
thus V is open by A1,TDLAT_3:15;
thus x in V by TARSKI:def 1;
thus not y in V by A2,TARSKI:def 1;
end;
hence
(ex V being Subset of Y st V is open & x in V & not y in V) or ex W
being Subset of Y st W is open & not x in W & y in W;
end;
hence thesis;
end;
cluster non T_0 -> non discrete for non empty TopSpace;
coherence;
cluster anti-discrete non trivial -> non T_0 for non empty TopSpace;
coherence by Lm1;
cluster anti-discrete T_0 -> trivial for non empty TopSpace;
coherence;
cluster T_0 non trivial -> non anti-discrete for non empty TopSpace;
coherence;
end;
Lm2: for X being non empty TopSpace, x being Point of X holds x in Cl {x}
proof
let X be non empty TopSpace, x be Point of X;
x in {x} & {x} c= Cl {x} by PRE_TOPC:18,TARSKI:def 1;
hence thesis;
end;
definition
let X be non empty TopSpace;
redefine attr X is T_0 means :: redefines T_0 (TSP_1, redefinition) → T_0 (TSP_1, redefinition) → T_0 (PRE_TOPC, definition)
for x, y being Point of X st x <> y holds Cl {x} <> Cl {y};
compatibility
proof
thus X is T_0 implies for x, y being Point of X st x <> y holds Cl {x} <>
Cl {y}
proof
assume
A1: X is T_0;
hereby
let x, y be Point of X;
assume
A2: x <> y;
now
per cases by A1,A2;
suppose
ex V being Subset of X st V is open & x in V & not y in V;
then consider V being Subset of X such that
A3: V is open and
A4: x in V and
A5: not y in V;
x in {x} & {x} c= Cl {x} by PRE_TOPC:18,TARSKI:def 1;
then
A6: (Cl {x}) /\ V <> {} by A4,XBOOLE_0:def 4;
y in V` by A5,SUBSET_1:29;
then {y} c= V` by ZFMISC_1:31;
then {y} misses V by SUBSET_1:23;
then
A7: Cl {y} misses V by A3,TSEP_1:36;
assume Cl {x} = Cl {y};
hence contradiction by A7,A6,XBOOLE_0:def 7;
end;
suppose
ex W being Subset of X st W is open & not x in W & y in W;
then consider W being Subset of X such that
A8: W is open and
A9: not x in W and
A10: y in W;
y in {y} & {y} c= Cl {y} by PRE_TOPC:18,TARSKI:def 1;
then
A11: (Cl {y}) /\ W <> {} by A10,XBOOLE_0:def 4;
x in W` by A9,SUBSET_1:29;
then {x} c= W` by ZFMISC_1:31;
then {x} misses W by SUBSET_1:23;
then
A12: (Cl {x}) misses W by A8,TSEP_1:36;
assume Cl {x} = Cl {y};
hence contradiction by A12,A11,XBOOLE_0:def 7;
end;
end;
hence Cl {x} <> Cl {y};
end;
end;
assume
A13: for x, y being Point of X st x <> y holds Cl {x} <> Cl {y};
now
let x, y be Point of X;
assume
A14: x <> y;
assume
A15: for E being Subset of X st E is closed & x in E holds y in E;
thus ex F being Subset of X st F is closed & not x in F & y in F
proof
set F = Cl {y};
take F;
thus F is closed;
now
assume x in F;
then {x} c= F by ZFMISC_1:31;
then
A16: Cl {x} c= F by TOPS_1:5;
y in Cl {x} by A15,Lm2;
then {y} c= Cl {x} by ZFMISC_1:31;
then F c= Cl {x} by TOPS_1:5;
then Cl {x} = F by A16,XBOOLE_0:def 10;
hence contradiction by A13,A14;
end;
hence not x in F;
thus thesis by Lm2;
end;
end;
hence thesis;
end;
end;
definition
let X be non empty TopSpace;
redefine attr X is T_0 means :: redefines T_0 (TSP_1, redefinition) → T_0 (TSP_1, redefinition) → T_0 (TSP_1, redefinition) → T_0 (PRE_TOPC, definition)
for x, y being Point of X st x <> y holds not x in Cl {y} or not y in Cl {x};
compatibility
proof
thus X is T_0 implies for x, y being Point of X st x <> y holds not x in
Cl {y} or not y in Cl {x}
proof
assume
A1: X is T_0;
hereby
let x, y be Point of X;
assume
A2: x <> y;
assume that
A3: x in Cl {y} and
A4: y in Cl {x};
{y} c= Cl {x} by A4,ZFMISC_1:31;
then
A5: Cl {y} c= Cl {x} by TOPS_1:5;
{x} c= Cl {y} by A3,ZFMISC_1:31;
then Cl {x} c= Cl {y} by TOPS_1:5;
then Cl {x} = Cl {y} by A5,XBOOLE_0:def 10;
hence contradiction by A1,A2;
end;
end;
assume
A6: for x, y being Point of X st x <> y holds not x in Cl {y} or not
y in Cl {x};
for x, y being Point of X st x <> y holds Cl {x} <> Cl {y}
proof
let x, y be Point of X;
assume
A7: x <> y;
assume
A8: Cl {x} = Cl {y};
now
per cases by A6,A7;
suppose
not x in Cl {y};
hence contradiction by A8,Lm2;
end;
suppose
not y in Cl {x};
hence contradiction by A8,Lm2;
end;
end;
hence contradiction;
end;
hence thesis;
end;
end;
definition
let X be non empty TopSpace;
redefine attr X is T_0 means :: redefines T_0 (TSP_1, redefinition) → T_0 (TSP_1, redefinition) → T_0 (TSP_1, redefinition) → T_0 (TSP_1, redefinition) → T_0 (PRE_TOPC, definition)
for x, y being Point of X st x <> y & x in Cl {
y} holds not Cl {y} c= Cl {x};
compatibility
proof
thus X is T_0 implies for x, y being Point of X st x <> y & x in Cl {y}
holds not Cl {y} c= Cl {x}
proof
assume
A1: X is T_0;
hereby
let x, y be Point of X;
assume
A2: x <> y;
assume x in Cl {y};
then {x} c= Cl {y} by ZFMISC_1:31;
then
A3: Cl {x} c= Cl {y} by TOPS_1:5;
assume Cl {y} c= Cl {x};
then Cl {x} = Cl {y} by A3,XBOOLE_0:def 10;
hence contradiction by A1,A2;
end;
end;
assume
A4: for x, y being Point of X st x <> y & x in Cl {y} holds not Cl {y}
c= Cl {x};
for x, y being Point of X st x <> y holds not x in Cl {y} or not y in
Cl {x}
proof
let x, y be Point of X;
assume
A5: x <> y;
assume
A6: x in Cl {y};
assume y in Cl {x};
then {y} c= Cl {x} by ZFMISC_1:31;
hence contradiction by A4,A5,A6,TOPS_1:5;
end;
hence thesis;
end;
end;
registration
cluster almost_discrete T_0 -> discrete for non empty TopSpace;
coherence
proof
let Y be non empty TopSpace;
assume
A1: Y is almost_discrete T_0;
for A being Subset of Y, x being Point of Y st A = {x} holds A is closed
proof
let A be Subset of Y, x be Point of Y;
x in Cl {x} by Lm2;
then
A2: {x} c= Cl {x} by ZFMISC_1:31;
A3: now
assume not Cl {x} c= {x};
then consider a being object such that
A4: a in Cl {x} and
A5: not a in {x} by TARSKI:def 3;
reconsider a as Point of Y by A4;
a <> x by A5,TARSKI:def 1;
then not x in Cl {a} by A1,A4;
then x in (Cl {a})` by SUBSET_1:29;
then {x} c= (Cl {a})` by ZFMISC_1:31;
then
A6: {x} misses Cl {a} by SUBSET_1:23;
A7: a in {a} & {a} c= Cl {a} by PRE_TOPC:18,TARSKI:def 1;
Cl {a} is open by A1,TDLAT_3:22;
then (Cl {x}) misses Cl {a} by A6,TSEP_1:36;
hence contradiction by A4,A7,XBOOLE_0:3;
end;
assume A = {x};
hence thesis by A2,A3,XBOOLE_0:def 10;
end;
hence thesis by A1,TDLAT_3:26;
end;
cluster almost_discrete non discrete -> non T_0 for non empty TopSpace;
coherence;
cluster non discrete T_0 -> non almost_discrete for non empty TopSpace;
coherence;
end;
definition
mode Kolmogorov_space is T_0 non empty TopSpace;
mode non-Kolmogorov_space is non T_0 non empty TopSpace;
end;
registration
cluster non trivial strict for Kolmogorov_space;
existence
proof
set X = the non trivial discrete strict non empty TopSpace;
take X;
thus thesis;
end;
cluster non trivial strict for non-Kolmogorov_space;
existence
proof
set X = the non trivial anti-discrete strict non empty TopSpace;
take X;
thus thesis;
end;
end;
begin
:: 3. T_{0} Subsets.
definition
let Y be TopStruct;
let IT be Subset of Y;
attr IT is T_0 means
for x, y being Point of Y st x in IT & y in IT &
x <> y holds (ex V being Subset of Y st V is open & x in V & not y in V) or ex
W being Subset of Y st W is open & not x in W & y in W;
end;
definition
let Y be non empty TopStruct;
let A be Subset of Y;
redefine attr A is T_0 means :: redefines T_0 (TSP_1, definition)
for x, y being Point of Y st x in A & y
in A & x <> y holds (ex E being Subset of Y st E is closed & x in E & not y in
E) or ex F being Subset of Y st F is closed & not x in F & y in F;
compatibility
proof
thus A is T_0 implies for x, y being Point of Y st x in A & y in A & x <>
y holds (ex E being Subset of Y st E is closed & x in E & not y in E) or ex F
being Subset of Y st F is closed & not x in F & y in F
proof
assume
A1: for x, y being Point of Y st x in A & y in A & x <> y holds (ex
V being Subset of Y st V is open & x in V & not y in V) or ex W being Subset of
Y st W is open & not x in W & y in W;
let x, y be Point of Y;
assume
A2: x in A & y in A & x <> y;
hereby
per cases by A1,A2;
suppose
ex V being Subset of Y st V is open & x in V & not y in V;
then consider V being Subset of Y such that
A3: V is open and
A4: x in V and
A5: not y in V;
now
take F = V`;
V = [#]Y \ F by PRE_TOPC:3;
hence F is closed by A3,PRE_TOPC:def 3;
thus not x in F by A4,XBOOLE_0:def 5;
thus y in F by A5,SUBSET_1:29;
end;
hence thesis;
end;
suppose
ex W being Subset of Y st W is open & not x in W & y in W;
then consider W being Subset of Y such that
A6: W is open and
A7: not x in W and
A8: y in W;
now
take E = W`;
W = [#]Y \ E by PRE_TOPC:3;
hence E is closed by A6,PRE_TOPC:def 3;
thus x in E by A7,SUBSET_1:29;
thus not y in E by A8,XBOOLE_0:def 5;
end;
hence thesis;
end;
end;
end;
assume
A9: for x, y being Point of Y st x in A & y in A & x <> y holds (ex E
being Subset of Y st E is closed & x in E & not y in E) or ex F being Subset of
Y st F is closed & not x in F & y in F;
for x, y being Point of Y st x in A & y in A & x <> y holds (ex V
being Subset of Y st V is open & x in V & not y in V) or ex W being Subset of Y
st W is open & not x in W & y in W
proof
let x, y be Point of Y;
assume
A10: x in A & y in A & x <> y;
hereby
per cases by A9,A10;
suppose
ex E being Subset of Y st E is closed & x in E & not y in E;
then consider E being Subset of Y such that
A11: E is closed and
A12: x in E and
A13: not y in E;
now
take W = E`;
W = [#]Y \ E;
hence W is open by A11,PRE_TOPC:def 3;
thus not x in W by A12,XBOOLE_0:def 5;
thus y in W by A13,SUBSET_1:29;
end;
hence thesis;
end;
suppose
ex F being Subset of Y st F is closed & not x in F & y in F;
then consider F being Subset of Y such that
A14: F is closed and
A15: not x in F and
A16: y in F;
now
take V = F`;
V = [#]Y \ F;
hence V is open by A14,PRE_TOPC:def 3;
thus x in V by A15,SUBSET_1:29;
thus not y in V by A16,XBOOLE_0:def 5;
end;
hence thesis;
end;
end;
end;
hence thesis;
end;
end;
theorem
for Y0, Y1 being TopStruct, D0 being Subset of Y0, D1 being Subset of
Y1 st the TopStruct of Y0 = the TopStruct of Y1 & D0 = D1 holds D0 is T_0
implies D1 is T_0
proof
let Y0, Y1 be TopStruct, D0 be Subset of Y0, D1 be Subset of Y1;
assume
A1: the TopStruct of Y0 = the TopStruct of Y1;
assume
A2: D0 = D1;
assume
A3: D0 is T_0;
now
let x, y be Point of Y1;
reconsider x0 = x, y0 = y as Point of Y0 by A1;
assume
A4: x in D1 & y in D1;
assume
A5: x <> y;
hereby
per cases by A2,A3,A4,A5;
suppose
ex V being Subset of Y0 st V is open & x0 in V & not y0 in V;
then consider V being Subset of Y0 such that
A6: V is open and
A7: x0 in V & not y0 in V;
reconsider V1 = V as Subset of Y1 by A1;
now
take V1;
V1 in the topology of Y1 by A1,A6,PRE_TOPC:def 2;
hence V1 is open by PRE_TOPC:def 2;
thus x in V1 & not y in V1 by A7;
end;
hence (ex V1 being Subset of Y1 st V1 is open & x in V1 & not y in V1)
or ex W1 being Subset of Y1 st W1 is open & not x in W1 & y in W1;
end;
suppose
ex W being Subset of Y0 st W is open & not x0 in W & y0 in W;
then consider W being Subset of Y0 such that
A8: W is open and
A9: ( not x0 in W)& y0 in W;
reconsider W1 = W as Subset of Y1 by A1;
now
take W1;
W1 in the topology of Y1 by A1,A8,PRE_TOPC:def 2;
hence W1 is open by PRE_TOPC:def 2;
thus not x in W1 & y in W1 by A9;
end;
hence (ex V1 being Subset of Y1 st V1 is open & x in V1 & not y in V1)
or ex W1 being Subset of Y1 st W1 is open & not x in W1 & y in W1;
end;
end;
end;
hence thesis;
end;
theorem Th4:
for Y being non empty TopStruct, A being Subset of Y st
A = the carrier of Y holds A is T_0 iff Y is T_0;
reserve Y for non empty TopStruct;
theorem Th5:
for A, B being Subset of Y st B c= A holds A is T_0 implies B is T_0;
theorem Th6:
for A, B being Subset of Y holds A is T_0 or B is T_0 implies A /\ B is T_0
proof
let A, B be Subset of Y;
assume
A1: A is T_0 or B is T_0;
hereby
per cases by A1;
suppose
A is T_0;
hence thesis by Th5,XBOOLE_1:17;
end;
suppose
B is T_0;
hence thesis by Th5,XBOOLE_1:17;
end;
end;
end;
theorem Th7:
for A, B being Subset of Y st A is open or B is open holds A is
T_0 & B is T_0 implies A \/ B is T_0
proof
let A, B be Subset of Y;
assume
A1: A is open or B is open;
assume that
A2: A is T_0 and
A3: B is T_0;
now
let x, y be Point of Y;
assume
A4: x in A \/ B & y in A \/ B;
then
A5: x in (A \ B) \/ B & y in (A \ B) \/ B by XBOOLE_1:39;
assume
A6: x <> y;
A7: x in A \/ (B \ A) & y in A \/ (B \ A) by A4,XBOOLE_1:39;
now
per cases by A1;
suppose
A8: A is open;
now
per cases by A7,XBOOLE_0:def 3;
suppose
x in A & y in A;
hence (ex V being Subset of Y st V is open & x in V & not y in V)
or ex W being Subset of Y st W is open & not x in W & y in W by A2,A6;
end;
suppose
A9: x in A & y in B \ A;
now
take A;
thus A is open by A8;
thus x in A by A9;
thus not y in A by A9,XBOOLE_0:def 5;
end;
hence (ex V being Subset of Y st V is open & x in V & not y in V)
or ex W being Subset of Y st W is open & not x in W & y in W;
end;
suppose
A10: x in B \ A & y in A;
now
take A;
thus A is open by A8;
thus not x in A by A10,XBOOLE_0:def 5;
thus y in A by A10;
end;
hence (ex V being Subset of Y st V is open & x in V & not y in V)
or ex W being Subset of Y st W is open & not x in W & y in W;
end;
suppose
A11: x in B \ A & y in B \ A;
B \ A c= B by XBOOLE_1:36;
hence (ex V being Subset of Y st V is open & x in V & not y in V)
or ex W being Subset of Y st W is open & not x in W & y in W by A3,A6,A11;
end;
end;
hence
(ex V being Subset of Y st V is open & x in V & not y in V) or ex
W being Subset of Y st W is open & not x in W & y in W;
end;
suppose
A12: B is open;
now
per cases by A5,XBOOLE_0:def 3;
suppose
A13: x in A \ B & y in A \ B;
A \ B c= A by XBOOLE_1:36;
hence (ex V being Subset of Y st V is open & x in V & not y in V)
or ex W being Subset of Y st W is open & not x in W & y in W by A2,A6,A13;
end;
suppose
A14: x in A \ B & y in B;
now
take B;
thus B is open by A12;
thus not x in B by A14,XBOOLE_0:def 5;
thus y in B by A14;
end;
hence (ex V being Subset of Y st V is open & x in V & not y in V)
or ex W being Subset of Y st W is open & not x in W & y in W;
end;
suppose
A15: x in B & y in A \ B;
now
take B;
thus B is open by A12;
thus x in B by A15;
thus not y in B by A15,XBOOLE_0:def 5;
end;
hence (ex V being Subset of Y st V is open & x in V & not y in V)
or ex W being Subset of Y st W is open & not x in W & y in W;
end;
suppose
x in B & y in B;
hence (ex V being Subset of Y st V is open & x in V & not y in V)
or ex W being Subset of Y st W is open & not x in W & y in W by A3,A6;
end;
end;
hence
(ex V being Subset of Y st V is open & x in V & not y in V) or ex
W being Subset of Y st W is open & not x in W & y in W;
end;
end;
hence (ex V being Subset of Y st V is open & x in V & not y in V) or ex W
being Subset of Y st W is open & not x in W & y in W;
end;
hence thesis;
end;
theorem Th8:
for A, B being Subset of Y st A is closed or B is closed holds A
is T_0 & B is T_0 implies A \/ B is T_0
proof
let A, B be Subset of Y;
assume
A1: A is closed or B is closed;
assume that
A2: A is T_0 and
A3: B is T_0;
now
let x, y be Point of Y;
assume
A4: x in A \/ B & y in A \/ B;
then
A5: x in (A \ B) \/ B & y in (A \ B) \/ B by XBOOLE_1:39;
assume
A6: x <> y;
A7: x in A \/ (B \ A) & y in A \/ (B \ A) by A4,XBOOLE_1:39;
now
per cases by A1;
suppose
A8: A is closed;
now
per cases by A7,XBOOLE_0:def 3;
suppose
x in A & y in A;
hence
(ex V being Subset of Y st V is closed & x in V & not y in V)
or ex W being Subset of Y st W is closed & not x in W & y in W by A2,A6;
end;
suppose
A9: x in A & y in B \ A;
now
take A;
thus A is closed by A8;
thus x in A by A9;
thus not y in A by A9,XBOOLE_0:def 5;
end;
hence
(ex V being Subset of Y st V is closed & x in V & not y in V)
or ex W being Subset of Y st W is closed & not x in W & y in W;
end;
suppose
A10: x in B \ A & y in A;
now
take A;
thus A is closed by A8;
thus not x in A by A10,XBOOLE_0:def 5;
thus y in A by A10;
end;
hence
(ex V being Subset of Y st V is closed & x in V & not y in V)
or ex W being Subset of Y st W is closed & not x in W & y in W;
end;
suppose
A11: x in B \ A & y in B \ A;
B \ A c= B by XBOOLE_1:36;
hence
(ex V being Subset of Y st V is closed & x in V & not y in V)
or ex W being Subset of Y st W is closed & not x in W & y in W by A3,A6,A11;
end;
end;
hence (ex V being Subset of Y st V is closed & x in V & not y in V) or
ex W being Subset of Y st W is closed & not x in W & y in W;
end;
suppose
A12: B is closed;
now
per cases by A5,XBOOLE_0:def 3;
suppose
A13: x in A \ B & y in A \ B;
A \ B c= A by XBOOLE_1:36;
hence
(ex V being Subset of Y st V is closed & x in V & not y in V)
or ex W being Subset of Y st W is closed & not x in W & y in W by A2,A6,A13;
end;
suppose
A14: x in A \ B & y in B;
now
take B;
thus B is closed by A12;
thus not x in B by A14,XBOOLE_0:def 5;
thus y in B by A14;
end;
hence
(ex V being Subset of Y st V is closed & x in V & not y in V)
or ex W being Subset of Y st W is closed & not x in W & y in W;
end;
suppose
A15: x in B & y in A \ B;
now
take B;
thus B is closed by A12;
thus x in B by A15;
thus not y in B by A15,XBOOLE_0:def 5;
end;
hence
(ex V being Subset of Y st V is closed & x in V & not y in V)
or ex W being Subset of Y st W is closed & not x in W & y in W;
end;
suppose
x in B & y in B;
hence
(ex V being Subset of Y st V is closed & x in V & not y in V)
or ex W being Subset of Y st W is closed & not x in W & y in W by A3,A6;
end;
end;
hence (ex V being Subset of Y st V is closed & x in V & not y in V) or
ex W being Subset of Y st W is closed & not x in W & y in W;
end;
end;
hence
(ex V being Subset of Y st V is closed & x in V & not y in V) or ex W
being Subset of Y st W is closed & not x in W & y in W;
end;
hence thesis;
end;
theorem Th9:
for A being Subset of Y holds A is discrete implies A is T_0
proof
let A be Subset of Y;
assume
A1: A is discrete;
now
let x, y be Point of Y;
assume that
A2: x in A and
A3: y in A;
{x} c= A by A2,ZFMISC_1:31;
then consider G being Subset of Y such that
A4: G is open and
A5: A /\ G = {x} by A1,TEX_2:def 3;
assume
A6: x <> y;
now
take G;
thus G is open by A4;
x in {x} by TARSKI:def 1;
hence x in G by A5,XBOOLE_0:def 4;
now
assume y in G;
then y in {x} by A3,A5,XBOOLE_0:def 4;
hence contradiction by A6,TARSKI:def 1;
end;
hence not y in G;
end;
hence (ex V being Subset of Y st V is open & x in V & not y in V) or ex W
being Subset of Y st W is open & not x in W & y in W;
end;
hence thesis;
end;
theorem
for A being non empty Subset of Y holds A is anti-discrete & A is not
trivial implies A is not T_0
proof
let A be non empty Subset of Y;
assume
A1: A is anti-discrete;
consider s being object such that
A2: s in A by XBOOLE_0:def 1;
reconsider s0 = s as Element of A by A2;
assume A is not trivial;
then A <> {s0};
then consider t being object such that
A3: t in A and
A4: t <> s0 by ZFMISC_1:35;
reconsider s, t as Point of Y by A2,A3;
assume
A5: A is T_0;
now
per cases by A3,A4,A5;
suppose
ex E being Subset of Y st E is closed & s in E & not t in E;
then consider E being Subset of Y such that
A6: E is closed & s in E and
A7: not t in E;
A c= E by A1,A2,A6,TEX_4:def 2;
hence contradiction by A3,A7;
end;
suppose
ex F being Subset of Y st F is closed & not s in F & t in F;
then consider F being Subset of Y such that
A8: F is closed and
A9: not s in F and
A10: t in F;
A c= F by A1,A3,A8,A10,TEX_4:def 2;
hence contradiction by A2,A9;
end;
end;
hence contradiction;
end;
definition
let X be non empty TopSpace;
let A be Subset of X;
redefine attr A is T_0 means :: redefines T_0 (TSP_1, redefinition) → T_0 (TSP_1, definition)
for x, y being Point of X st x in A & y in A & x <> y holds Cl {x} <> Cl {y};
compatibility
proof
thus A is T_0 implies for x, y being Point of X st x in A & y in A & x <>
y holds Cl {x} <> Cl {y}
proof
assume
A1: A is T_0;
hereby
let x, y be Point of X;
assume
A2: x in A & y in A & x <> y;
now
per cases by A1,A2;
suppose
ex V being Subset of X st V is open & x in V & not y in V;
then consider V being Subset of X such that
A3: V is open and
A4: x in V and
A5: not y in V;
y in V` by A5,SUBSET_1:29;
then {y} c= V` by ZFMISC_1:31;
then
A6: {y} misses V by SUBSET_1:23;
assume
A7: Cl {x} = Cl {y};
x in {x} & {x} c= Cl {x} by PRE_TOPC:18,TARSKI:def 1;
then (Cl {x}) meets V by A4,XBOOLE_0:3;
hence contradiction by A3,A6,A7,TSEP_1:36;
end;
suppose
ex W being Subset of X st W is open & not x in W & y in W;
then consider W being Subset of X such that
A8: W is open and
A9: not x in W and
A10: y in W;
x in W` by A9,SUBSET_1:29;
then {x} c= W` by ZFMISC_1:31;
then
A11: {x} misses W by SUBSET_1:23;
assume
A12: Cl {x} = Cl {y};
y in {y} & {y} c= Cl {y} by PRE_TOPC:18,TARSKI:def 1;
then (Cl {y}) meets W by A10,XBOOLE_0:3;
hence contradiction by A8,A11,A12,TSEP_1:36;
end;
end;
hence Cl {x} <> Cl {y};
end;
end;
assume
A13: for x, y being Point of X st x in A & y in A & x <> y holds Cl {x
} <> Cl {y};
now
let x, y be Point of X;
assume
A14: x in A & y in A & x <> y;
assume
A15: for E being Subset of X st E is closed & x in E holds y in E;
thus ex F being Subset of X st F is closed & not x in F & y in F
proof
set F = Cl {y};
take F;
thus F is closed;
now
assume x in F;
then {x} c= F by ZFMISC_1:31;
then
A16: Cl {x} c= F by TOPS_1:5;
y in Cl {x} by A15,Lm2;
then {y} c= Cl {x} by ZFMISC_1:31;
then F c= Cl {x} by TOPS_1:5;
then Cl {x} = F by A16,XBOOLE_0:def 10;
hence contradiction by A13,A14;
end;
hence not x in F;
thus thesis by Lm2;
end;
end;
hence thesis;
end;
end;
definition
let X be non empty TopSpace;
let A be Subset of X;
redefine attr A is T_0 means :: redefines T_0 (TSP_1, redefinition) → T_0 (TSP_1, redefinition) → T_0 (TSP_1, definition)
for x, y being Point of X st x in A & y
in A & x <> y holds not x in Cl {y} or not y in Cl {x};
compatibility
proof
thus A is T_0 implies for x, y being Point of X st x in A & y in A & x <>
y holds not x in Cl {y} or not y in Cl {x}
proof
assume
A1: A is T_0;
hereby
let x, y be Point of X;
assume
A2: x in A & y in A & x <> y;
assume that
A3: x in Cl {y} and
A4: y in Cl {x};
{y} c= Cl {x} by A4,ZFMISC_1:31;
then
A5: Cl {y} c= Cl {x} by TOPS_1:5;
{x} c= Cl {y} by A3,ZFMISC_1:31;
then Cl {x} c= Cl {y} by TOPS_1:5;
then Cl {x} = Cl {y} by A5,XBOOLE_0:def 10;
hence contradiction by A1,A2;
end;
end;
assume
A6: for x, y being Point of X st x in A & y in A & x <> y holds not x
in Cl {y} or not y in Cl {x};
for x, y being Point of X st x in A & y in A & x <> y holds Cl {x} <>
Cl {y}
proof
let x, y be Point of X;
assume
A7: x in A & y in A & x <> y;
assume
A8: Cl {x} = Cl {y};
now
per cases by A6,A7;
suppose
not x in Cl {y};
hence contradiction by A8,Lm2;
end;
suppose
not y in Cl {x};
hence contradiction by A8,Lm2;
end;
end;
hence contradiction;
end;
hence thesis;
end;
end;
definition
let X be non empty TopSpace;
let A be Subset of X;
redefine attr A is T_0 means :: redefines T_0 (TSP_1, redefinition) → T_0 (TSP_1, redefinition) → T_0 (TSP_1, redefinition) → T_0 (TSP_1, definition)
for x, y being Point of X st x in A & y in A &
x <> y holds x in Cl {y} implies not Cl {y} c= Cl {x};
compatibility
proof
thus A is T_0 implies for x, y being Point of X st x in A & y in A & x <>
y holds x in Cl {y} implies not Cl {y} c= Cl {x}
proof
assume
A1: A is T_0;
hereby
let x, y be Point of X;
assume
A2: x in A & y in A & x <> y;
assume x in Cl {y};
then {x} c= Cl {y} by ZFMISC_1:31;
then
A3: Cl {x} c= Cl {y} by TOPS_1:5;
assume Cl {y} c= Cl {x};
then Cl {x} = Cl {y} by A3,XBOOLE_0:def 10;
hence contradiction by A1,A2;
end;
end;
assume
A4: for x, y being Point of X st x in A & y in A & x <> y holds x in
Cl {y} implies not Cl {y} c= Cl {x};
for x, y being Point of X st x in A & y in A & x <> y holds not x in
Cl {y} or not y in Cl {x}
proof
let x, y be Point of X;
assume
A5: x in A & y in A & x <> y;
assume
A6: x in Cl {y};
assume y in Cl {x};
then {y} c= Cl {x} by ZFMISC_1:31;
hence contradiction by A4,A5,A6,TOPS_1:5;
end;
hence thesis;
end;
end;
reserve X for non empty TopSpace;
theorem
for A being empty Subset of X holds A is T_0;
theorem
for x being Point of X holds {x} is T_0 by Th9,TEX_2:30;
begin
:: 4. Kolmogorov Subspaces.
registration
let Y be non empty TopStruct;
cluster strict T_0 non empty for SubSpace of Y;
existence
proof
set X0 = the trivial strict non empty SubSpace of Y;
take X0;
thus thesis;
end;
end;
Lm3: now
let Z be TopStruct;
let Z0 be SubSpace of Z;
[#]Z0 c= [#]Z by PRE_TOPC:def 4;
hence the carrier of Z0 is Subset of Z;
end;
definition
let Y be TopStruct;
let Y0 be SubSpace of Y;
redefine attr Y0 is T_0 means :: redefines T_0 (TSP_1, redefinition) → T_0 (TSP_1, redefinition) → T_0 (PRE_TOPC, definition)
Y0 is empty or for x, y being Point of Y st x
is Point of Y0 & y is Point of Y0 & x <> y holds (ex V being Subset of Y st V
is open & x in V & not y in V) or ex W being Subset of Y st W is open & not x
in W & y in W;
compatibility
proof
reconsider A = the carrier of Y0 as Subset of Y by Lm3;
thus Y0 is T_0 implies Y0 is empty or for x, y being Point of Y st x is
Point of Y0 & y is Point of Y0 & x <> y holds (ex V being Subset of Y st V is
open & x in V & not y in V) or ex W being Subset of Y st W is open & not x in W
& y in W
proof
assume
A1: Y0 is T_0;
hereby
assume
A2: Y0 is non empty;
let x, y be Point of Y;
assume x is Point of Y0 & y is Point of Y0;
then reconsider x0 = x, y0 = y as Point of Y0;
assume
A3: x <> y;
now
per cases by A1,A2,A3;
suppose
ex E0 being Subset of Y0 st E0 is open & x0 in E0 & not y0 in E0;
then consider E0 being Subset of Y0 such that
A4: E0 is open and
A5: x0 in E0 and
A6: not y0 in E0;
now
consider E being Subset of Y such that
A7: E is open and
A8: E0 = E /\ A by A4,Def1;
take E;
thus E is open by A7;
E /\ A c= E by XBOOLE_1:17;
hence x in E by A5,A8;
thus not y in E by A2,A6,A8,XBOOLE_0:def 4;
end;
hence (ex E being Subset of Y st E is open & x in E & not y in E)
or ex F being Subset of Y st F is open & not x in F & y in F;
end;
suppose
ex F0 being Subset of Y0 st F0 is open & not x0 in F0 & y0 in F0;
then consider F0 being Subset of Y0 such that
A9: F0 is open and
A10: not x0 in F0 and
A11: y0 in F0;
now
consider F being Subset of Y such that
A12: F is open and
A13: F0 = F /\ A by A9,Def1;
take F;
thus F is open by A12;
thus not x in F by A2,A10,A13,XBOOLE_0:def 4;
F /\ A c= F by XBOOLE_1:17;
hence y in F by A11,A13;
end;
hence (ex E being Subset of Y st E is open & x in E & not y in E)
or ex F being Subset of Y st F is open & not x in F & y in F;
end;
end;
hence
(ex E being Subset of Y st E is open & x in E & not y in E) or ex
F being Subset of Y st F is open & not x in F & y in F;
end;
end;
assume
A14: Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y
is Point of Y0 & x <> y holds (ex V being Subset of Y st V is open & x in V &
not y in V) or ex W being Subset of Y st W is open & not x in W & y in W;
now
A15: the carrier of Y0 c= the carrier of Y by Def1;
assume
A16: Y0 is non empty;
let x0, y0 be Point of Y0;
the carrier of Y0 <> {} by A16;
then x0 in the carrier of Y0 & y0 in the carrier of Y0;
then reconsider x = x0, y = y0 as Point of Y by A15;
assume
A17: x0 <> y0;
now
per cases by A14,A16,A17;
suppose
ex E being Subset of Y st E is open & x in E & not y in E;
then consider E being Subset of Y such that
A18: E is open and
A19: x in E and
A20: not y in E;
now
consider E0 being Subset of Y0 such that
A21: E0 is open and
A22: E0 = E /\ A by A18,Th1;
take E0;
thus E0 is open by A21;
thus x0 in E0 by A16,A19,A22,XBOOLE_0:def 4;
now
A23: E /\ A c= E by XBOOLE_1:17;
assume y0 in E0;
hence contradiction by A20,A22,A23;
end;
hence not y0 in E0;
end;
hence (ex E0 being Subset of Y0 st E0 is open & x0 in E0 & not y0 in
E0) or ex F0 being Subset of Y0 st F0 is open & not x0 in F0 & y0 in F0;
end;
suppose
ex F being Subset of Y st F is open & not x in F & y in F;
then consider F being Subset of Y such that
A24: F is open and
A25: not x in F and
A26: y in F;
now
consider F0 being Subset of Y0 such that
A27: F0 is open and
A28: F0 = F /\ A by A24,Th1;
take F0;
thus F0 is open by A27;
now
A29: F /\ A c= F by XBOOLE_1:17;
assume x0 in F0;
hence contradiction by A25,A28,A29;
end;
hence not x0 in F0;
thus y0 in F0 by A16,A26,A28,XBOOLE_0:def 4;
end;
hence (ex E0 being Subset of Y0 st E0 is open & x0 in E0 & not y0 in
E0) or ex F0 being Subset of Y0 st F0 is open & not x0 in F0 & y0 in F0;
end;
end;
hence (ex E0 being Subset of Y0 st E0 is open & x0 in E0 & not y0 in E0)
or ex F0 being Subset of Y0 st F0 is open & not x0 in F0 & y0 in F0;
end;
hence thesis;
end;
end;
definition
let Y be TopStruct;
let Y0 be SubSpace of Y;
redefine attr Y0 is T_0 means :: redefines T_0 (TSP_1, redefinition) → T_0 (TSP_1, redefinition) → T_0 (PRE_TOPC, definition)
Y0 is empty or for x, y being Point of
Y st x is Point of Y0 & y is Point of Y0 & x <> y holds (ex E being Subset of Y
st E is closed & x in E & not y in E) or ex F being Subset of Y st F is closed
& not x in F & y in F;
compatibility
proof
reconsider A = the carrier of Y0 as Subset of Y by Lm3;
thus Y0 is T_0 implies Y0 is empty or for x, y being Point of Y st x is
Point of Y0 & y is Point of Y0 & x <> y holds (ex E being Subset of Y st E is
closed & x in E & not y in E) or ex F being Subset of Y st F is closed & not x
in F & y in F
proof
assume
A1: Y0 is T_0;
hereby
assume
A2: Y0 is not empty;
let x, y be Point of Y;
assume x is Point of Y0 & y is Point of Y0;
then reconsider x0 = x, y0 = y as Point of Y0;
assume
A3: x <> y;
now
per cases by A1,A2,A3;
suppose
ex E0 being Subset of Y0 st E0 is closed & x0 in E0 & not y0 in E0;
then consider E0 being Subset of Y0 such that
A4: E0 is closed and
A5: x0 in E0 and
A6: not y0 in E0;
now
consider E being Subset of Y such that
A7: E is closed and
A8: E0 = E /\ A by A4,Def2;
take E;
thus E is closed by A7;
E /\ A c= E by XBOOLE_1:17;
hence x in E by A5,A8;
thus not y in E by A2,A6,A8,XBOOLE_0:def 4;
end;
hence
(ex E being Subset of Y st E is closed & x in E & not y in E)
or ex F being Subset of Y st F is closed & not x in F & y in F;
end;
suppose
ex F0 being Subset of Y0 st F0 is closed & not x0 in F0 & y0 in F0;
then consider F0 being Subset of Y0 such that
A9: F0 is closed and
A10: not x0 in F0 and
A11: y0 in F0;
now
consider F being Subset of Y such that
A12: F is closed and
A13: F0 = F /\ A by A9,Def2;
take F;
thus F is closed by A12;
thus not x in F by A2,A10,A13,XBOOLE_0:def 4;
F /\ A c= F by XBOOLE_1:17;
hence y in F by A11,A13;
end;
hence
(ex E being Subset of Y st E is closed & x in E & not y in E)
or ex F being Subset of Y st F is closed & not x in F & y in F;
end;
end;
hence (ex E being Subset of Y st E is closed & x in E & not y in E) or
ex F being Subset of Y st F is closed & not x in F & y in F;
end;
end;
assume
A14: Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y
is Point of Y0 & x <> y holds (ex E being Subset of Y st E is closed & x in E &
not y in E) or ex F being Subset of Y st F is closed & not x in F & y in F;
now
A15: the carrier of Y0 c= the carrier of Y by Def1;
assume
A16: Y0 is not empty;
let x0, y0 be Point of Y0;
the carrier of Y0 <> {} by A16;
then x0 in the carrier of Y0 & y0 in the carrier of Y0;
then reconsider x = x0, y = y0 as Point of Y by A15;
assume
A17: x0 <> y0;
now
per cases by A14,A16,A17;
suppose
ex E being Subset of Y st E is closed & x in E & not y in E;
then consider E being Subset of Y such that
A18: E is closed and
A19: x in E and
A20: not y in E;
now
consider E0 being Subset of Y0 such that
A21: E0 is closed and
A22: E0 = E /\ A by A18,Th2;
take E0;
thus E0 is closed by A21;
thus x0 in E0 by A16,A19,A22,XBOOLE_0:def 4;
now
A23: E /\ A c= E by XBOOLE_1:17;
assume y0 in E0;
hence contradiction by A20,A22,A23;
end;
hence not y0 in E0;
end;
hence (ex E0 being Subset of Y0 st E0 is closed & x0 in E0 & not y0
in E0) or ex F0 being Subset of Y0 st F0 is closed & not x0 in F0 & y0 in F0;
end;
suppose
ex F being Subset of Y st F is closed & not x in F & y in F;
then consider F being Subset of Y such that
A24: F is closed and
A25: not x in F and
A26: y in F;
now
consider F0 being Subset of Y0 such that
A27: F0 is closed and
A28: F0 = F /\ A by A24,Th2;
take F0;
thus F0 is closed by A27;
now
A29: F /\ A c= F by XBOOLE_1:17;
assume x0 in F0;
hence contradiction by A25,A28,A29;
end;
hence not x0 in F0;
thus y0 in F0 by A16,A26,A28,XBOOLE_0:def 4;
end;
hence (ex E0 being Subset of Y0 st E0 is closed & x0 in E0 & not y0
in E0) or ex F0 being Subset of Y0 st F0 is closed & not x0 in F0 & y0 in F0;
end;
end;
hence
(ex E0 being Subset of Y0 st E0 is closed & x0 in E0 & not y0 in E0
) or ex F0 being Subset of Y0 st F0 is closed & not x0 in F0 & y0 in F0;
end;
hence thesis;
end;
end;
reserve Y for non empty TopStruct;
theorem Th13:
for Y0 being non empty SubSpace of Y, A being Subset of Y st
A = the carrier of Y0 holds A is T_0 iff Y0 is T_0;
theorem
for Y0 being non empty SubSpace of Y, Y1 being T_0 non empty SubSpace
of Y st Y0 is SubSpace of Y1 holds Y0 is T_0
proof
let Y0 be non empty SubSpace of Y, Y1 be T_0 non empty SubSpace of Y;
reconsider A1 = the carrier of Y1, A0 = the carrier of Y0 as non empty
Subset of Y by Lm3;
assume
A1: Y0 is SubSpace of Y1;
A2: A1 is T_0 by Th13;
[#]Y0 = A0 & [#]Y1 = A1;
then A0 c= A1 by A1,PRE_TOPC:def 4;
then A0 is T_0 by A2;
hence thesis;
end;
reserve X for non empty TopSpace;
theorem
for X1 being T_0 non empty SubSpace of X, X2 being non empty SubSpace
of X holds X1 meets X2 implies X1 meet X2 is T_0
proof
let X1 be T_0 non empty SubSpace of X, X2 be non empty SubSpace of X;
reconsider A1 = the carrier of X1 as non empty Subset of X by TSEP_1:1;
reconsider A2 = the carrier of X2 as non empty Subset of X by TSEP_1:1;
assume X1 meets X2;
then
A1: the carrier of X1 meet X2 = A1 /\ A2 by TSEP_1:def 4;
A1 is T_0 by Th13;
then A1 /\ A2 is T_0 by Th6;
hence thesis by A1;
end;
theorem
for X1, X2 being T_0 non empty SubSpace of X holds X1 is open or X2 is
open implies X1 union X2 is T_0
proof
let X1, X2 be T_0 non empty SubSpace of X;
reconsider A1 = the carrier of X1, A2 = the carrier of X2 as non empty
Subset of X by TSEP_1:1;
assume X1 is open or X2 is open;
then
A1: A1 is open or A2 is open by TSEP_1:16;
A1 is T_0 & A2 is T_0 by Th13;
then the carrier of X1 union X2 = A1 \/ A2 & A1 \/ A2 is T_0 by A1,Th7,
TSEP_1:def 2;
hence thesis;
end;
theorem
for X1, X2 being T_0 non empty SubSpace of X holds X1 is closed or X2
is closed implies X1 union X2 is T_0
proof
let X1, X2 be T_0 non empty SubSpace of X;
reconsider A1 = the carrier of X1, A2 = the carrier of X2 as non empty
Subset of X by TSEP_1:1;
assume X1 is closed or X2 is closed;
then
A1: A1 is closed or A2 is closed by TSEP_1:11;
A1 is T_0 & A2 is T_0 by Th13;
then the carrier of X1 union X2 = A1 \/ A2 & A1 \/ A2 is T_0 by A1,Th8,
TSEP_1:def 2;
hence thesis;
end;
definition
let X be non empty TopSpace;
mode Kolmogorov_subspace of X is T_0 non empty SubSpace of X;
end;
theorem
for X being non empty TopSpace, A0 being non empty Subset of X st A0
is T_0 ex X0 being strict Kolmogorov_subspace of X st A0 = the carrier of X0
proof
let X be non empty TopSpace, A0 be non empty Subset of X;
consider X0 being strict non empty SubSpace of X such that
A1: A0 = the carrier of X0 by TSEP_1:10;
assume A0 is T_0;
then reconsider X0 as strict Kolmogorov_subspace of X by A1,Th13;
take X0;
thus thesis by A1;
end;
registration
let X be non trivial TopSpace;
cluster proper strict for Kolmogorov_subspace of X;
existence
proof
set X0 = the trivial strict non empty SubSpace of X;
take X0;
thus thesis;
end;
end;
registration
let X be Kolmogorov_space;
cluster -> T_0 for non empty SubSpace of X;
coherence
proof
let X0 be non empty SubSpace of X;
reconsider A0 = the carrier of X0 as non empty Subset of X by TSEP_1:1;
X is SubSpace of X by TSEP_1:2;
then reconsider A = the carrier of X as non empty Subset of X by TSEP_1:1;
A is T_0 by Th4;
then A0 is T_0;
hence thesis;
end;
end;
registration
let X be non-Kolmogorov_space;
cluster non proper -> non T_0 for non empty SubSpace of X;
coherence
proof
let X0 be non empty SubSpace of X;
reconsider A0 = the carrier of X0 as non empty Subset of X by TSEP_1:1;
X is SubSpace of X by TSEP_1:2;
then reconsider A = the carrier of X as non empty Subset of X by TSEP_1:1;
assume X0 is non proper;
then A0 is not proper by TEX_2:8;
then A0 = A;
then A0 is not T_0 by Th4;
hence thesis;
end;
cluster T_0 -> proper for non empty SubSpace of X;
coherence;
end;
registration
let X be non-Kolmogorov_space;
cluster strict non T_0 for SubSpace of X;
existence
proof
set X0 = the non proper strict non empty SubSpace of X;
take X0;
thus thesis;
end;
end;
definition
let X be non-Kolmogorov_space;
mode non-Kolmogorov_subspace of X is non T_0 SubSpace of X;
end;
theorem
for X being non empty non-Kolmogorov_space, A0 being Subset of X st A0
is not T_0 ex X0 being strict non-Kolmogorov_subspace of X st A0 = the carrier
of X0
proof
let X be non empty non-Kolmogorov_space, A0 be Subset of X;
assume
A1: A0 is not T_0;
then A0 is non empty;
then consider X0 being strict non empty SubSpace of X such that
A2: A0 = the carrier of X0 by TSEP_1:10;
reconsider X0 as non T_0 strict SubSpace of X by A1,A2,Th13;
take X0;
thus thesis by A2;
end;