Volume 6, 1994

University of Bialystok

Copyright (c) 1994 Association of Mizar Users

### The abstract of the Mizar article:

### On Kolmogorov Topological Spaces

**by****Zbigniew Karno**- Received July 26, 1994
- MML identifier: TSP_1

- [ Mizar article, MML identifier index ]

environ vocabulary PRE_TOPC, BOOLE, SUBSET_1, METRIC_1, REALSET1, TDLAT_3, NATTRA_1, SETFAM_1, TARSKI, COLLSP, TSP_1; notation TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, BORSUK_1, TSEP_1, TDLAT_3, TEX_1, TEX_2, T_0TOPSP, TEX_4; constructors REALSET1, TSEP_1, TDLAT_3, TEX_2, T_0TOPSP, TEX_4, BORSUK_1, MEMBERED; clusters TDLAT_3, TEX_1, TEX_2, STRUCT_0, MEMBERED, ZFMISC_1; requirements SUBSET, BOOLE; begin :: 1. Subspaces. definition let Y be TopStruct; redefine mode SubSpace of Y -> TopStruct 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; canceled; theorem :: TSP_1:2 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 -> TopStruct 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; canceled; theorem :: TSP_1:4 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 discerning 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); synonym T is T_0; 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; definition cluster trivial -> T_0 (non empty TopStruct); cluster non T_0 -> non trivial (non empty TopStruct); end; definition cluster strict T_0 non empty TopSpace; cluster strict non T_0 non empty TopSpace; end; definition cluster discrete -> T_0 (non empty TopSpace); cluster non T_0 -> non discrete (non empty TopSpace); cluster anti-discrete non trivial -> non T_0 (non empty TopSpace); cluster anti-discrete T_0 -> trivial (non empty TopSpace); cluster T_0 non trivial -> non anti-discrete (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; definition cluster almost_discrete T_0 -> discrete (non empty TopSpace); cluster almost_discrete non discrete -> non T_0 (non empty TopSpace); cluster non discrete T_0 -> non almost_discrete (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; definition cluster non trivial strict Kolmogorov_space; cluster non trivial strict 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:5 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:6 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:7 for A, B being Subset of Y st B c= A holds A is T_0 implies B is T_0; theorem :: TSP_1:8 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:9 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:10 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:11 for A being Subset of Y holds A is discrete implies A is T_0; theorem :: TSP_1:12 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:13 for A being empty Subset of X holds A is T_0; theorem :: TSP_1:14 for x being Point of X holds {x} is T_0; begin :: 4. Kolmogorov Subspaces. definition let Y be non empty TopStruct; cluster strict T_0 non empty 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:15 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:16 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:17 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:18 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:19 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:20 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; definition let X be non trivial (non empty TopSpace); cluster proper strict Kolmogorov_subspace of X; end; definition let X be Kolmogorov_space; cluster -> T_0 (non empty SubSpace of X); end; definition let X be non-Kolmogorov_space; cluster non proper -> non T_0 (non empty SubSpace of X); cluster T_0 -> proper (non empty SubSpace of X); end; definition let X be non-Kolmogorov_space; cluster strict non T_0 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:21 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;

Back to top