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

:: 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 & a <> b holds
compatibility
( A is T_0 iff for a, b being Point of X st a in A & b in A & a <> b holds
proof end;
end;

:: deftheorem 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 & b in A & a <> b holds

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 /\ () = {a};
compatibility
( A is T_0 iff for a being Point of X st a in A holds
A /\ () = {a} )
proof end;
end;

:: deftheorem 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 /\ () = {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 & 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 & A /\ D = {a} ) )
proof end;
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 & A /\ D = {a} ) );

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;

:: deftheorem 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 & ( for D being Subset of Y st D is T_0 & 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 #) & D0 = D1 & D0 is maximal_T_0 holds
D1 is maximal_T_0
proof end;

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 );
compatibility
( M is maximal_T_0 iff ( M is T_0 & MaxADSet M = the carrier of X ) )
proof end;
end;

:: deftheorem 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 & 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
proof end;

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 ) & A is maximal_T_0 holds
not A is proper by ;

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
proof end;

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)
proof end;

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)
proof end;

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 :: TSP_2:def 6
for x being Point of X ex a being Point of X st
( a in M & M /\ () = {a} );
compatibility
( M is maximal_T_0 iff for x being Point of X ex a being Point of X st
( a in M & M /\ () = {a} ) )
proof end;
end;

:: deftheorem 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 & M /\ () = {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 & M is maximal_T_0 )
proof end;

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

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

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

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 V59() for SubSpace of Y;
coherence
for b1 being non empty SubSpace of Y st b1 is maximal_T_0 holds
b1 is V59()
proof end;
cluster non empty V59() -> non empty non maximal_T_0 for SubSpace of Y;
coherence
for b1 being non empty SubSpace of Y st b1 is V59() 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 V59() & ( for Y0 being non empty V59() 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 V59() & ( for Y0 being non empty V59() 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 #) ) ) )
proof end;
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 V59() & ( for Y0 being non empty V59() 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 & A0 = the carrier of X0 )
proof end;

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
proof end;
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 & b1 is maximal_T_0 holds
not b1 is proper
proof end;
cluster open proper -> non maximal_T_0 for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is open & 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 & 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 & b1 is maximal_T_0 holds
not b1 is proper
proof end;
cluster closed proper -> non maximal_T_0 for SubSpace of X;
coherence
for b1 being SubSpace of X st b1 is closed & 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 & 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 V59() SubSpace of X ex X0 being strict SubSpace of X st
( Y0 is SubSpace of X0 & X0 is maximal_T_0 )
proof end;

registration
let X be non empty TopSpace;
existence
ex b1 being SubSpace of X st
( b1 is maximal_T_0 & b1 is strict & not b1 is empty )
proof end;
end;

definition 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 & G0 = () /\ the carrier of X0 ) )
proof end;

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 & ex G0 being Subset of X0 st
( G0 is open & G0 = G /\ the carrier of X0 ) ) )
proof end;

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 & F0 = () /\ the carrier of X0 ) )
proof end;

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 & ex F0 being Subset of X0 st
( F0 is closed & F0 = F /\ the carrier of X0 ) ) )
proof end;

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 & ( for a being Point of X holds M /\ () = {(r . a)} ) holds
r is continuous Function of X,X0
proof end;

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
proof end;

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 & ( for a being Point of X holds M /\ () = {(r . a)} ) holds
r is being_a_retraction
proof end;

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
proof end;

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
proof end;

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
proof end;

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}

proof end;

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 /\ () = {(r . a)}

proof end;

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}

proof end;

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

proof end;

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

proof end;

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 & b2 is being_a_retraction holds
b1 = b2
proof end;
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} by ;

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

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

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 /\ () = {(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 /\ () = {(b1 . a)} )
proof end;
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 /\ () = {(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 )
proof end;
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
proof end;

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)) .: ()
proof end;

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 /\ () = 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 /\ () = b1 .: A )
proof end;
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 /\ () = 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
proof end;

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)) .: ()
proof end;

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)
proof end;

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)
proof end;

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)
proof end;

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
proof end;

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
proof end;