:: Maximal Kolmogorov Subspaces of a Topological Space as Stone Retracts of the Ambient Space
:: by Zbigniew Karno
::
:: Received July 26, 1994
:: Copyright (c) 1994-2012 Association of Mizar Users


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 :Def1: :: TSP_2:def 1
 for a, b being Point of X st a in A &amp; b in A &amp; a <> b holds
MaxADSet a misses MaxADSet b;
compatibility
 ( A is T_0 iff for a, b being Point of X st a in A &amp; b in A &amp; a <> b holds
MaxADSet a misses MaxADSet b )
proofend;
end;

:: deftheorem Def1 defines T_0 TSP_2:def_1_:_
 for X being non empty TopSpace
for A being Subset of X holds
( A is T_0 iff for a, b being Point of X st a in A &amp; b in A &amp; a <> b holds
MaxADSet a misses MaxADSet b );

definition
let X be non empty TopSpace;
let A be Subset of X;
redefine attr A is T_0  means :Def2: :: TSP_2:def 2
 for a being Point of X st a in A holds
A /\ (MaxADSet a) = {a};
compatibility
 ( A is T_0 iff for a being Point of X st a in A holds
A /\ (MaxADSet a) = {a} )
proofend;
end;

:: deftheorem Def2 defines T_0 TSP_2:def_2_:_
 for X being non empty TopSpace
for A being Subset of X holds
( A is T_0 iff for a being Point of X st a in A holds
A /\ (MaxADSet a) = {a} );

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 holds
ex D being Subset of X st
( D is maximal_anti-discrete &amp; A /\ D = {a} );
compatibility
 ( A is T_0 iff for a being Point of X st a in A holds
ex D being Subset of X st
( D is maximal_anti-discrete &amp; A /\ D = {a} ) )
proofend;
end;

:: deftheorem  defines T_0 TSP_2:def_3_:_
 for X being non empty TopSpace
for A being Subset of X holds
( A is T_0 iff for a being Point of X st a in A holds
ex D being Subset of X st
( D is maximal_anti-discrete &amp; A /\ D = {a} ) );

definition
let Y be TopStruct ;
let IT be Subset of Y;
attrIT is maximal_T_0  means :Def4: :: TSP_2:def 4
( IT is T_0 &amp; ( for D being Subset of Y st D is T_0 &amp; IT c= D holds
IT = D ) );
end;

:: deftheorem Def4 defines maximal_T_0 TSP_2:def_4_:_
 for Y being TopStruct
for IT being Subset of Y holds
( IT is maximal_T_0 iff ( IT is T_0 &amp; ( for D being Subset of Y st D is T_0 &amp; IT c= D holds
IT = D ) ) );

theorem :: TSP_2:1
for Y0, Y1 being TopStruct
for D0 being Subset of Y0
for D1 being Subset of Y1 st TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) &amp; D0 = D1 &amp; D0 is maximal_T_0 holds
D1 is maximal_T_0
proofend;

definition
let X be non empty TopSpace;
let M be Subset of X;
redefine attr M is maximal_T_0  means :Def5: :: TSP_2:def 5
( M is T_0 &amp; MaxADSet M = the carrier of X );
compatibility
 ( M is maximal_T_0 iff ( M is T_0 &amp; MaxADSet M = the carrier of X ) )
proofend;
end;

:: deftheorem Def5 defines maximal_T_0 TSP_2:def_5_:_
 for X being non empty TopSpace
for M being Subset of X holds
( M is maximal_T_0 iff ( M is T_0 &amp; MaxADSet M = the carrier of X ) );

theorem Th2: :: TSP_2:2
for X being non empty TopSpace
for M being Subset of X st M is maximal_T_0 holds
M is dense
proofend;

theorem Th3: :: TSP_2:3
for X being non empty TopSpace
for A being Subset of X st ( A is open or A is closed ) &amp; A is maximal_T_0 holds
not A is proper
proofend;

theorem Th4: :: TSP_2:4
for X being non empty TopSpace
for A being empty Subset of X holds not A is maximal_T_0
proofend;

theorem Th5: :: TSP_2:5
for X being non empty TopSpace
for M being Subset of X st M is maximal_T_0 holds
for A being Subset of X st A is closed holds
A = MaxADSet (M /\ A)
proofend;

theorem Th6: :: TSP_2:6
for X being non empty TopSpace
for M being Subset of X st M is maximal_T_0 holds
for A being Subset of X st A is open holds
A = MaxADSet (M /\ A)
proofend;

theorem :: TSP_2:7
for X being non empty TopSpace
for M being Subset of X st M is maximal_T_0 holds
for A being Subset of X holds Cl A = MaxADSet (M /\ (Cl A)) by Th5;

theorem :: TSP_2:8
for X being non empty TopSpace
for M being Subset of X st M is maximal_T_0 holds
for A being Subset of X holds Int A = MaxADSet (M /\ (Int A)) by Th6;

definition
let X be non empty TopSpace;
let M be Subset of X;
redefine attr M is maximal_T_0  means :Def6: :: TSP_2:def 6
 for x being Point of X ex a being Point of X st
( a in M &amp; M /\ (MaxADSet x) = {a} );
compatibility
 ( M is maximal_T_0 iff for x being Point of X ex a being Point of X st
( a in M &amp; M /\ (MaxADSet x) = {a} ) )
proofend;
end;

:: deftheorem Def6 defines maximal_T_0 TSP_2:def_6_:_
 for X being non empty TopSpace
for M being Subset of X holds
( M is maximal_T_0 iff for x being Point of X ex a being Point of X st
( a in M &amp; M /\ (MaxADSet x) = {a} ) );

theorem Th9: :: TSP_2:9
for X being non empty TopSpace
for A being Subset of X st A is T_0 holds
ex M being Subset of X st
( A c= M &amp; M is maximal_T_0 )
proofend;

theorem Th10: :: TSP_2:10
for X being non empty TopSpace ex M being Subset of X st M is maximal_T_0
proofend;

begin

:: 2. Maximal Kolmogorov Subspaces.
definition
let Y be non empty TopStruct ;
let IT be SubSpace of Y;
attrIT is maximal_T_0  means :Def7: :: TSP_2:def 7
 for A being Subset of Y st A = the carrier of IT holds
A is maximal_T_0 ;
end;

:: deftheorem Def7 defines maximal_T_0 TSP_2:def_7_:_
 for Y being non empty TopStruct
for IT being SubSpace of Y holds
( IT is maximal_T_0 iff for A being Subset of Y st A = the carrier of IT holds
A is maximal_T_0 );

theorem Th11: :: TSP_2:11
for Y being non empty TopStruct
for Y0 being SubSpace of Y
for A being Subset of Y st A = the carrier of Y0 holds
( A is maximal_T_0 iff Y0 is maximal_T_0 )
proofend;

Lm1: now__::_thesis:_for_Z_being_non_empty_TopStruct_
for_Z0_being_SubSpace_of_Z_holds_the_carrier_of_Z0_is_Subset_of_Z
let Z be non empty TopStruct ; ::_thesis: for Z0 being SubSpace of Z holds the carrier of Z0 is Subset of Z
let Z0 be SubSpace of Z; ::_thesis: the carrier of Z0 is Subset of Z
 [#] Z0 c= [#] Z by PRE_TOPC:def_4;
hence  the carrier of Z0 is Subset of Z ; ::_thesis: verum
end;

registration
let Y be non empty TopStruct ;
cluster non empty maximal_T_0  ->  non empty V56() for SubSpace of Y;
coherence
 for b1 being non empty SubSpace of Y st b1 is maximal_T_0 holds
b1 is V56()
proofend;
cluster non empty V56()  ->  non empty non maximal_T_0 for SubSpace of Y;
coherence
 for b1 being non empty SubSpace of Y st b1 is V56() holds
not b1 is maximal_T_0 ;
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 V56() &amp; ( for Y0 being non empty V56() SubSpace of X st X0 is SubSpace of Y0 holds
TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) );
compatibility
 ( X0 is maximal_T_0 iff ( X0 is V56() &amp; ( for Y0 being non empty V56() SubSpace of X st X0 is SubSpace of Y0 holds
TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) ) )
proofend;
end;

:: deftheorem  defines maximal_T_0 TSP_2:def_8_:_
 for X being non empty TopSpace
for X0 being non empty SubSpace of X holds
( X0 is maximal_T_0 iff ( X0 is V56() &amp; ( for Y0 being non empty V56() SubSpace of X st X0 is SubSpace of Y0 holds
TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) ) );

theorem Th12: :: TSP_2:12
for X being non empty TopSpace
for A0 being non empty Subset of X st A0 is maximal_T_0 holds
ex X0 being non empty strict SubSpace of X st
( X0 is maximal_T_0 &amp; A0 = the carrier of X0 )
proofend;

registration
let X be non empty TopSpace;
cluster maximal_T_0  ->  dense for SubSpace of X;
coherence
 for b1 being SubSpace of X st b1 is maximal_T_0 holds
b1 is dense
proofend;
cluster non dense  ->  non maximal_T_0 for SubSpace of X;
coherence
 for b1 being SubSpace of X st not b1 is dense holds
not b1 is maximal_T_0 ;
cluster open maximal_T_0  ->  non proper for SubSpace of X;
coherence
 for b1 being SubSpace of X st b1 is open &amp; b1 is maximal_T_0 holds
not b1 is proper
proofend;
cluster open proper  ->  non maximal_T_0 for SubSpace of X;
coherence
 for b1 being SubSpace of X st b1 is open &amp; b1 is proper holds
not b1 is maximal_T_0 ;
cluster proper maximal_T_0  ->  non open for SubSpace of X;
coherence
 for b1 being SubSpace of X st b1 is proper &amp; b1 is maximal_T_0 holds
not b1 is open ;
cluster closed maximal_T_0  ->  non proper for SubSpace of X;
coherence
 for b1 being SubSpace of X st b1 is closed &amp; b1 is maximal_T_0 holds
not b1 is proper
proofend;
cluster closed proper  ->  non maximal_T_0 for SubSpace of X;
coherence
 for b1 being SubSpace of X st b1 is closed &amp; b1 is proper holds
not b1 is maximal_T_0 ;
cluster proper maximal_T_0  ->  non closed for SubSpace of X;
coherence
 for b1 being SubSpace of X st b1 is proper &amp; b1 is maximal_T_0 holds
not b1 is closed ;
end;

theorem :: TSP_2:13
for X being non empty TopSpace
for Y0 being non empty V56() SubSpace of X ex X0 being strict SubSpace of X st
( Y0 is SubSpace of X0 &amp; X0 is maximal_T_0 )
proofend;

registration
let X be non empty TopSpace;
cluster non empty strict TopSpace-like maximal_T_0 for SubSpace of X;
existence
 ex b1 being SubSpace of X st
( b1 is maximal_T_0 &amp; b1 is strict &amp; not b1 is empty )
proofend;
end;

definition
let X be non empty TopSpace;
mode maximal_Kolmogorov_subspace of X is maximal_T_0 SubSpace of X;
end;

theorem Th14: :: TSP_2:14
for X being non empty TopSpace
for X0 being maximal_Kolmogorov_subspace of X
for G being Subset of X
for G0 being Subset of X0 st G0 = G holds
( G0 is open iff ( MaxADSet G is open &amp; G0 = (MaxADSet G) /\ the carrier of X0 ) )
proofend;

theorem :: TSP_2:15
for X being non empty TopSpace
for X0 being maximal_Kolmogorov_subspace of X
for G being Subset of X holds
( G is open iff ( G = MaxADSet G &amp; ex G0 being Subset of X0 st
( G0 is open &amp; G0 = G /\ the carrier of X0 ) ) )
proofend;

theorem Th16: :: TSP_2:16
for X being non empty TopSpace
for X0 being maximal_Kolmogorov_subspace of X
for F being Subset of X
for F0 being Subset of X0 st F0 = F holds
( F0 is closed iff ( MaxADSet F is closed &amp; F0 = (MaxADSet F) /\ the carrier of X0 ) )
proofend;

theorem :: TSP_2:17
for X being non empty TopSpace
for X0 being maximal_Kolmogorov_subspace of X
for F being Subset of X holds
( F is closed iff ( F = MaxADSet F &amp; ex F0 being Subset of X0 st
( F0 is closed &amp; F0 = F /\ the carrier of X0 ) ) )
proofend;

begin

theorem Th18: :: TSP_2:18
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for r being Function of X,X0
for M being Subset of X st M = the carrier of X0 &amp; ( for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) holds
r is continuous Function of X,X0
proofend;

theorem :: TSP_2:19
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for r being Function of X,X0 st ( for a being Point of X holds r . a in MaxADSet a ) holds
r is continuous Function of X,X0
proofend;

theorem Th20: :: TSP_2:20
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for r being continuous Function of X,X0
for M being Subset of X st M = the carrier of X0 &amp; ( for a being Point of X holds M /\ (MaxADSet a) = {(r . a)} ) holds
r is being_a_retraction
proofend;

theorem Th21: :: TSP_2:21
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for r being continuous Function of X,X0 st ( for a being Point of X holds r . a in MaxADSet a ) holds
r is being_a_retraction
proofend;

theorem Th22: :: TSP_2:22
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X ex r being continuous Function of X,X0 st r is being_a_retraction
proofend;

theorem :: TSP_2:23
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X holds X0 is_a_retract_of X
proofend;

Lm2:  for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for a being Point of X
for b being Point of X0 st a = b holds
r " (Cl {b}) = Cl {a}
proofend;

Lm3:  for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for A being Subset of X st A = the carrier of X0 holds
for a being Point of X holds A /\ (MaxADSet a) = {(r . a)}
proofend;

Lm4:  for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for a being Point of X
for b being Point of X0 st a = b holds
MaxADSet a c= r " {b}
proofend;

Lm5:  for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for a being Point of X
for b being Point of X0 st a = b holds
r " {b} = MaxADSet a
proofend;

Lm6:  for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for E being Subset of X
for F being Subset of X0 st F = E holds
r " F = MaxADSet E
proofend;

definition
let X be non empty TopSpace;
let X0 be non empty maximal_Kolmogorov_subspace of X;
func Stone-retraction (X,X0) ->  continuous Function of X,X0 means :Def9: :: TSP_2:def 9
it is being_a_retraction ;
existence
 ex b1 being continuous Function of X,X0 st b1 is being_a_retraction by Th22;
uniqueness
 for b1, b2 being continuous Function of X,X0 st b1 is being_a_retraction &amp; b2 is being_a_retraction holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines Stone-retraction TSP_2:def_9_:_
 for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for b3 being continuous Function of X,X0 holds
( b3 = Stone-retraction (X,X0) iff b3 is being_a_retraction );

theorem :: TSP_2:24
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for a being Point of X
for b being Point of X0 st a = b holds
(Stone-retraction (X,X0)) " (Cl {b}) = Cl {a}
proofend;

theorem Th25: :: TSP_2:25
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for a being Point of X
for b being Point of X0 st a = b holds
(Stone-retraction (X,X0)) " {b} = MaxADSet a
proofend;

theorem Th26: :: TSP_2:26
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for E being Subset of X
for F being Subset of X0 st F = E holds
(Stone-retraction (X,X0)) " F = MaxADSet E
proofend;

definition
let X be non empty TopSpace;
let X0 be non empty maximal_Kolmogorov_subspace of X;
redefine func Stone-retraction (X,X0) means :Def10: :: TSP_2:def 10
 for M being Subset of X st M = the carrier of X0 holds
for a being Point of X holds M /\ (MaxADSet a) = {(it . a)};
compatibility
 for b1 being continuous Function of X,X0 holds
( b1 = Stone-retraction (X,X0) iff for M being Subset of X st M = the carrier of X0 holds
for a being Point of X holds M /\ (MaxADSet a) = {(b1 . a)} )
proofend;
end;

:: deftheorem Def10 defines Stone-retraction TSP_2:def_10_:_
 for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for b3 being continuous Function of X,X0 holds
( b3 = Stone-retraction (X,X0) iff for M being Subset of X st M = the carrier of X0 holds
for a being Point of X holds M /\ (MaxADSet a) = {(b3 . a)} );

definition
let X be non empty TopSpace;
let X0 be non empty maximal_Kolmogorov_subspace of X;
redefine func Stone-retraction (X,X0) means :Def11: :: TSP_2:def 11
 for a being Point of X holds it . a in MaxADSet a;
compatibility
 for b1 being continuous Function of X,X0 holds
( b1 = Stone-retraction (X,X0) iff for a being Point of X holds b1 . a in MaxADSet a )
proofend;
end;

:: deftheorem Def11 defines Stone-retraction TSP_2:def_11_:_
 for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for b3 being continuous Function of X,X0 holds
( b3 = Stone-retraction (X,X0) iff for a being Point of X holds b3 . a in MaxADSet a );

theorem Th27: :: TSP_2:27
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for a being Point of X holds (Stone-retraction (X,X0)) " {((Stone-retraction (X,X0)) . a)} = MaxADSet a
proofend;

theorem :: TSP_2:28
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for a being Point of X holds Im ((Stone-retraction (X,X0)),a) = (Stone-retraction (X,X0)) .: (MaxADSet a)
proofend;

definition
let X be non empty TopSpace;
let X0 be non empty maximal_Kolmogorov_subspace of X;
redefine func Stone-retraction (X,X0) means :Def12: :: TSP_2:def 12
 for M being Subset of X st M = the carrier of X0 holds
for A being Subset of X holds M /\ (MaxADSet A) = it .: A;
compatibility
 for b1 being continuous Function of X,X0 holds
( b1 = Stone-retraction (X,X0) iff for M being Subset of X st M = the carrier of X0 holds
for A being Subset of X holds M /\ (MaxADSet A) = b1 .: A )
proofend;
end;

:: deftheorem Def12 defines Stone-retraction TSP_2:def_12_:_
 for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for b3 being continuous Function of X,X0 holds
( b3 = Stone-retraction (X,X0) iff for M being Subset of X st M = the carrier of X0 holds
for A being Subset of X holds M /\ (MaxADSet A) = b3 .: A );

theorem Th29: :: TSP_2:29
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for A being Subset of X holds (Stone-retraction (X,X0)) " ((Stone-retraction (X,X0)) .: A) = MaxADSet A
proofend;

theorem :: TSP_2:30
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for A being Subset of X holds (Stone-retraction (X,X0)) .: A = (Stone-retraction (X,X0)) .: (MaxADSet A)
proofend;

theorem :: TSP_2:31
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for A, B being Subset of X holds (Stone-retraction (X,X0)) .: (A \/ B) = ((Stone-retraction (X,X0)) .: A) \/ ((Stone-retraction (X,X0)) .: B)
proofend;

theorem :: TSP_2:32
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
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)
proofend;

theorem :: TSP_2:33
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
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)
proofend;

theorem :: TSP_2:34
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for A being Subset of X st A is open holds
(Stone-retraction (X,X0)) .: A is open
proofend;

theorem :: TSP_2:35
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for A being Subset of X st A is closed holds
(Stone-retraction (X,X0)) .: A is closed
proofend;