:: On Kolmogorov Topological Spaces
:: by Zbigniew Karno
::
:: Received July 26, 1994
:: Copyright (c) 1994-2021 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;
begin
:: 1. Subspaces.
definition
let Y be TopStruct;
redefine mode SubSpace of Y means
:: TSP_1:def 1
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;
end;
theorem :: TSP_1:1
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;
definition
let Y be TopStruct;
redefine mode SubSpace of Y means
:: TSP_1:def 2
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;
end;
theorem :: TSP_1:2
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;
begin
:: 2. Kolmogorov Spaces.
definition
let T be TopStruct;
redefine attr T is T_0 means
:: TSP_1:def 3
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;
end;
definition
let Y be TopStruct;
redefine attr Y is T_0 means
:: TSP_1:def 4
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;
end;
registration
cluster trivial -> T_0 for non empty TopStruct;
end;
registration
cluster strict T_0 non empty for TopSpace;
cluster strict non T_0 non empty for TopSpace;
end;
registration
cluster discrete -> T_0 for non empty TopSpace;
cluster non T_0 -> non discrete for non empty TopSpace;
cluster anti-discrete non trivial -> non T_0 for non empty TopSpace;
cluster anti-discrete T_0 -> trivial for non empty TopSpace;
cluster T_0 non trivial -> non anti-discrete for non empty TopSpace;
end;
definition
let X be non empty TopSpace;
redefine attr X is T_0 means
:: TSP_1:def 5
for x, y being Point of X st x <> y holds Cl {x} <> Cl {y};
end;
definition
let X be non empty TopSpace;
redefine attr X is T_0 means
:: TSP_1:def 6
for x, y being Point of X st x <> y holds not x in Cl {y} or not y in Cl {x};
end;
definition
let X be non empty TopSpace;
redefine attr X is T_0 means
:: TSP_1:def 7
for x, y being Point of X st x <> y & x in Cl {
y} holds not Cl {y} c= Cl {x};
end;
registration
cluster almost_discrete T_0 -> discrete for non empty TopSpace;
cluster almost_discrete non discrete -> non T_0 for non empty TopSpace;
cluster non discrete T_0 -> non almost_discrete for non empty TopSpace;
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;
cluster non trivial strict for non-Kolmogorov_space;
end;
begin
:: 3. T_{0} Subsets.
definition
let Y be TopStruct;
let IT be Subset of Y;
attr IT is T_0 means
:: TSP_1:def 8
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
:: TSP_1:def 9
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;
end;
theorem :: TSP_1:3
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;
theorem :: TSP_1:4
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 :: TSP_1:5
for A, B being Subset of Y st B c= A holds A is T_0 implies B is T_0;
theorem :: TSP_1:6
for A, B being Subset of Y holds A is T_0 or B is T_0 implies A /\ B is T_0;
theorem :: TSP_1:7
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;
theorem :: TSP_1:8
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;
theorem :: TSP_1:9
for A being Subset of Y holds A is discrete implies A is T_0;
theorem :: TSP_1:10
for A being non empty Subset of Y holds A is anti-discrete & A is not
trivial implies A is not T_0;
definition
let X be non empty TopSpace;
let A be Subset of X;
redefine attr A is T_0 means
:: TSP_1:def 10
for x, y being Point of X st x in A & y in A & x <> y holds Cl {x} <> Cl {y};
end;
definition
let X be non empty TopSpace;
let A be Subset of X;
redefine attr A is T_0 means
:: TSP_1:def 11
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};
end;
definition
let X be non empty TopSpace;
let A be Subset of X;
redefine attr A is T_0 means
:: TSP_1:def 12
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};
end;
reserve X for non empty TopSpace;
theorem :: TSP_1:11
for A being empty Subset of X holds A is T_0;
theorem :: TSP_1:12
for x being Point of X holds {x} is T_0;
begin
:: 4. Kolmogorov Subspaces.
registration
let Y be non empty TopStruct;
cluster strict T_0 non empty for SubSpace of Y;
end;
definition
let Y be TopStruct;
let Y0 be SubSpace of Y;
redefine attr Y0 is T_0 means
:: TSP_1:def 13
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;
end;
definition
let Y be TopStruct;
let Y0 be SubSpace of Y;
redefine attr Y0 is T_0 means
:: TSP_1:def 14
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;
end;
reserve Y for non empty TopStruct;
theorem :: TSP_1:13
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 :: TSP_1:14
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;
reserve X for non empty TopSpace;
theorem :: TSP_1:15
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;
theorem :: TSP_1:16
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;
theorem :: TSP_1:17
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;
definition
let X be non empty TopSpace;
mode Kolmogorov_subspace of X is T_0 non empty SubSpace of X;
end;
theorem :: TSP_1:18
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;
registration
let X be non trivial TopSpace;
cluster proper strict for Kolmogorov_subspace of X;
end;
registration
let X be Kolmogorov_space;
cluster -> T_0 for non empty SubSpace of X;
end;
registration
let X be non-Kolmogorov_space;
cluster non proper -> non T_0 for non empty SubSpace of X;
cluster T_0 -> proper for non empty SubSpace of X;
end;
registration
let X be non-Kolmogorov_space;
cluster strict non T_0 for SubSpace of X;
end;
definition
let X be non-Kolmogorov_space;
mode non-Kolmogorov_subspace of X is non T_0 SubSpace of X;
end;
theorem :: TSP_1:19
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;