:: 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;