:: Maximal Kolmogorov Subspaces of a Topological Space as Stone
:: Retracts of the Ambient Space
:: by Zbigniew Karno
::
:: Received July 26, 1994
:: Copyright (c) 1994-2018 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;