Journal of Formalized Mathematics
Volume 6, 1994
University of Bialystok
Copyright (c) 1994 Association of Mizar Users

### Maximal Kolmogorov Subspaces of a Topological Space as Stone Retracts of the Ambient Space

by
Zbigniew Karno

MML identifier: TSP_2
[ Mizar article, MML identifier index ]

```environ

vocabulary PRE_TOPC, TSP_1, TEX_4, BOOLE, SUBSET_1, TARSKI, TOPS_1, COLLSP,
SETFAM_1, FUNCT_1, RELAT_1, NATTRA_1, ORDINAL2, BORSUK_1, TSP_2;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, RELAT_1, FUNCT_1,
FUNCT_2, PRE_TOPC, TOPS_1, BORSUK_1, TSEP_1, TEX_2, TEX_3, TEX_4, TSP_1;
constructors TOPS_1, TSEP_1, TEX_2, TEX_3, TEX_4, TSP_1, BORSUK_1, MEMBERED;
clusters PRE_TOPC, TSP_1, STRUCT_0, RELSET_1, SUBSET_1, BORSUK_1, MEMBERED,
ZFMISC_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
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;

definition let Y be non empty TopStruct;
cluster maximal_T_0 -> T_0 (non empty SubSpace of Y);
cluster non T_0 -> non maximal_T_0 (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;

definition let X be non empty TopSpace;
cluster maximal_T_0 -> dense SubSpace of X;
cluster non dense -> non maximal_T_0 SubSpace of X;
cluster open maximal_T_0 -> non proper SubSpace of X;
cluster open proper -> non maximal_T_0 SubSpace of X;
cluster proper maximal_T_0 -> non open SubSpace of X;
cluster closed maximal_T_0 -> non proper SubSpace of X;
cluster closed proper -> non maximal_T_0 SubSpace of X;
cluster proper maximal_T_0 -> non closed 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;

definition let X be non empty TopSpace;
cluster maximal_T_0 strict non empty 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 map 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 map of X,X0;

theorem :: TSP_2:19
for r being map of X,X0 holds
(for a being Point of X holds r.a in MaxADSet(a)) implies
r is continuous map of X,X0;

theorem :: TSP_2:20
for r being continuous map 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_a_retraction;

theorem :: TSP_2:21
for r being continuous map of X,X0 holds
(for a being Point of X holds r.a in MaxADSet(a)) implies
r is_a_retraction;

theorem :: TSP_2:22
ex r being continuous map of X,X0 st r is_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 map of X,X0 means
:: TSP_2:def 9
it is_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

theorem :: TSP_2:26
for E being Subset of X, F being Subset of X0
st F = E holds

definition let X be non empty TopSpace,
X0 be non empty maximal_Kolmogorov_subspace of X;
redefine func Stone-retraction(X,X0) -> continuous map of 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) -> continuous map of 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

theorem :: TSP_2:28
for a being Point of X holds

definition let X be non empty TopSpace,
X0 be non empty maximal_Kolmogorov_subspace of X;
redefine func Stone-retraction(X,X0) -> continuous map of 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

theorem :: TSP_2:30
for A being Subset of X holds

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