:: Maximal Kolmogorov Subspaces of a Topological Space as Stone :: Retracts of the Ambient Space :: 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 XBOOLE_0, PRE_TOPC, SUBSET_1, TEX_4, RCOMP_1, TARSKI, STRUCT_0, TOPS_1, ZFMISC_1, SETFAM_1, FUNCT_1, RELAT_1, NATTRA_1, ORDINAL2, BORSUK_1, TSP_2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, RELAT_1, RELSET_1, FUNCT_2, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, TSEP_1, TEX_2, TEX_3, TEX_4, TSP_1; constructors TOPS_1, BORSUK_1, TSEP_1, TEX_2, TEX_4, TSP_1, TEX_3; registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, PRE_TOPC, TOPS_1, TSP_1; requirements BOOLE, SUBSET; begin :: 1. Maximal T_{0} Subsets. definition let X be non empty TopSpace; let A be Subset of X; redefine attr A is T_0 means :: TSP_2:def 1 for a, b being Point of X st a in A & b in A holds a <> b implies MaxADSet(a) misses MaxADSet(b); end; definition let X be non empty TopSpace; let A be Subset of X; redefine attr A is T_0 means :: TSP_2:def 2 for a being Point of X st a in A holds A /\ MaxADSet(a) = {a}; end; definition let X be non empty TopSpace; let A be Subset of X; redefine attr A is T_0 means :: TSP_2:def 3 for a being Point of X st a in A ex D being Subset of X st D is maximal_anti-discrete & A /\ D = {a}; end; definition let Y be TopStruct; let IT be Subset of Y; attr IT is maximal_T_0 means :: TSP_2:def 4 IT is T_0 & for D being Subset of Y st D is T_0 & IT c= D holds IT = D; end; theorem :: TSP_2:1 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 maximal_T_0 implies D1 is maximal_T_0; definition let X be non empty TopSpace; let M be Subset of X; redefine attr M is maximal_T_0 means :: TSP_2:def 5 M is T_0 & MaxADSet(M) = the carrier of X; end; reserve X for non empty TopSpace; theorem :: TSP_2:2 for M being Subset of X holds M is maximal_T_0 implies M is dense; theorem :: TSP_2:3 for A being Subset of X st A is open or A is closed holds A is maximal_T_0 implies A is not proper; theorem :: TSP_2:4 for A being empty Subset of X holds A is not maximal_T_0; theorem :: TSP_2:5 for M being Subset of X st M is maximal_T_0 for A being Subset of X st A is closed holds A = MaxADSet(M /\ A); theorem :: TSP_2:6 for M being Subset of X st M is maximal_T_0 for A being Subset of X st A is open holds A = MaxADSet(M /\ A); theorem :: TSP_2:7 for M being Subset of X st M is maximal_T_0 for A being Subset of X holds Cl A = MaxADSet(M /\ Cl A); theorem :: TSP_2:8 for M being Subset of X st M is maximal_T_0 for A being Subset of X holds Int A = MaxADSet(M /\ Int A); definition let X be non empty TopSpace; let M be Subset of X; redefine attr M is maximal_T_0 means :: TSP_2:def 6 for x being Point of X ex a being Point of X st a in M & M /\ MaxADSet(x) = {a}; end; theorem :: TSP_2:9 for A being Subset of X holds A is T_0 implies ex M being Subset of X st A c= M & M is maximal_T_0; theorem :: TSP_2:10 ex M being Subset of X st M is maximal_T_0; begin :: 2. Maximal Kolmogorov Subspaces. definition let Y be non empty TopStruct; let IT be SubSpace of Y; attr IT is maximal_T_0 means :: TSP_2:def 7 for A being Subset of Y st A = the carrier of IT holds A is maximal_T_0; end; theorem :: TSP_2:11 for Y being non empty TopStruct, Y0 being SubSpace of Y, A being Subset of Y st A = the carrier of Y0 holds A is maximal_T_0 iff Y0 is maximal_T_0; registration let Y be non empty TopStruct; cluster maximal_T_0 -> T_0 for non empty SubSpace of Y; cluster non T_0 -> non maximal_T_0 for non empty SubSpace of Y; end; definition let X be non empty TopSpace; let X0 be non empty SubSpace of X; redefine attr X0 is maximal_T_0 means :: TSP_2:def 8 X0 is T_0 & for Y0 being T_0 non empty SubSpace of X st X0 is SubSpace of Y0 holds the TopStruct of X0 = the TopStruct of Y0; end; reserve X for non empty TopSpace; theorem :: TSP_2:12 for A0 being non empty Subset of X st A0 is maximal_T_0 ex X0 being strict non empty SubSpace of X st X0 is maximal_T_0 & A0 = the carrier of X0; registration let X be non empty TopSpace; cluster maximal_T_0 -> dense for SubSpace of X; cluster non dense -> non maximal_T_0 for SubSpace of X; cluster open maximal_T_0 -> non proper for SubSpace of X; cluster open proper -> non maximal_T_0 for SubSpace of X; cluster proper maximal_T_0 -> non open for SubSpace of X; cluster closed maximal_T_0 -> non proper for SubSpace of X; cluster closed proper -> non maximal_T_0 for SubSpace of X; cluster proper maximal_T_0 -> non closed for SubSpace of X; end; theorem :: TSP_2:13 for Y0 being T_0 non empty SubSpace of X ex X0 being strict SubSpace of X st Y0 is SubSpace of X0 & X0 is maximal_T_0; registration let X be non empty TopSpace; cluster maximal_T_0 strict non empty for SubSpace of X; end; definition let X be non empty TopSpace; mode maximal_Kolmogorov_subspace of X is maximal_T_0 SubSpace of X; end; theorem :: TSP_2:14 for X0 being maximal_Kolmogorov_subspace of X for G being Subset of X, G0 being Subset of X0 st G0 = G holds G0 is open iff MaxADSet(G) is open & G0 = MaxADSet(G) /\ the carrier of X0; theorem :: TSP_2:15 for X0 being maximal_Kolmogorov_subspace of X for G being Subset of X holds G is open iff G = MaxADSet(G) & ex G0 being Subset of X0 st G0 is open & G0 = G /\ the carrier of X0; theorem :: TSP_2:16 for X0 being maximal_Kolmogorov_subspace of X for F being Subset of X, F0 being Subset of X0 st F0 = F holds F0 is closed iff MaxADSet(F) is closed & F0 = MaxADSet(F) /\ the carrier of X0; theorem :: TSP_2:17 for X0 being maximal_Kolmogorov_subspace of X for F being Subset of X holds F is closed iff F = MaxADSet(F) & ex F0 being Subset of X0 st F0 is closed & F0 = F /\ the carrier of X0; begin :: 3. Stone Retraction Mapping Theorems. reserve X for non empty TopSpace, X0 for non empty maximal_Kolmogorov_subspace of X; theorem :: TSP_2:18 for r being Function of X,X0 for M being Subset of X st M = the carrier of X0 holds (for a being Point of X holds M /\ MaxADSet(a) = {r.a}) implies r is continuous Function of X,X0; theorem :: TSP_2:19 for r being Function of X,X0 holds (for a being Point of X holds r.a in MaxADSet(a)) implies r is continuous Function of X,X0; theorem :: TSP_2:20 for r being continuous Function of X,X0 for M being Subset of X st M = the carrier of X0 holds (for a being Point of X holds M /\ MaxADSet(a) = {r.a}) implies r is being_a_retraction; theorem :: TSP_2:21 for r being continuous Function of X,X0 holds (for a being Point of X holds r.a in MaxADSet(a)) implies r is being_a_retraction; theorem :: TSP_2:22 ex r being continuous Function of X,X0 st r is being_a_retraction; theorem :: TSP_2:23 X0 is_a_retract_of X; definition let X be non empty TopSpace, X0 be non empty maximal_Kolmogorov_subspace of X; func Stone-retraction(X,X0) -> continuous Function of X,X0 means :: TSP_2:def 9 it is being_a_retraction; end; theorem :: TSP_2:24 for a being Point of X, b being Point of X0 st a = b holds ( Stone-retraction(X,X0))" Cl {b} = Cl {a}; theorem :: TSP_2:25 for a being Point of X, b being Point of X0 st a = b holds ( Stone-retraction(X,X0))" {b} = MaxADSet(a); theorem :: TSP_2:26 for E being Subset of X, F being Subset of X0 st F = E holds ( Stone-retraction(X,X0))" (F) = MaxADSet(E); definition let X be non empty TopSpace, X0 be non empty maximal_Kolmogorov_subspace of X; redefine func Stone-retraction(X,X0) means :: TSP_2:def 10 for M being Subset of X st M = the carrier of X0 for a being Point of X holds M /\ MaxADSet(a) = {it.a}; end; definition let X be non empty TopSpace, X0 be non empty maximal_Kolmogorov_subspace of X; redefine func Stone-retraction(X,X0) means :: TSP_2:def 11 for a being Point of X holds it.a in MaxADSet(a); end; theorem :: TSP_2:27 for a being Point of X holds (Stone-retraction(X,X0))" {( Stone-retraction(X,X0)).a} = MaxADSet(a); theorem :: TSP_2:28 for a being Point of X holds Im(Stone-retraction(X,X0),a) = ( Stone-retraction(X,X0)).: MaxADSet(a); definition let X be non empty TopSpace, X0 be non empty maximal_Kolmogorov_subspace of X; redefine func Stone-retraction(X,X0) means :: TSP_2:def 12 for M being Subset of X st M = the carrier of X0 for A being Subset of X holds M /\ MaxADSet(A) = it.: A; end; theorem :: TSP_2:29 for A being Subset of X holds (Stone-retraction(X,X0))"(( Stone-retraction(X,X0)).: A) = MaxADSet(A); theorem :: TSP_2:30 for A being Subset of X holds (Stone-retraction(X,X0)).: A = ( Stone-retraction(X,X0)).: MaxADSet(A); theorem :: TSP_2:31 for A, B being Subset of X holds (Stone-retraction(X,X0)).:(A \/ B) = (Stone-retraction(X,X0)).:(A) \/ (Stone-retraction(X,X0)).:(B); theorem :: TSP_2:32 for A, B being Subset of X st A is open or B is open holds ( Stone-retraction(X,X0)).:(A /\ B) = (Stone-retraction(X,X0)).:(A) /\ ( Stone-retraction(X,X0)).:(B); theorem :: TSP_2:33 for A, B being Subset of X st A is closed or B is closed holds ( Stone-retraction(X,X0)).:(A /\ B) = (Stone-retraction(X,X0)).:(A) /\ ( Stone-retraction(X,X0)).:(B); theorem :: TSP_2:34 for A being Subset of X holds A is open implies (Stone-retraction(X,X0 )).:(A) is open; theorem :: TSP_2:35 for A being Subset of X holds A is closed implies (Stone-retraction(X, X0)).:(A) is closed;