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

begin

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 & b in A & 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 & b in A & a <> b holds
MaxADSet a misses MaxADSet b )

proof end;

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 & b in A & 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} )

proof end;

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 & 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 :Def4: :: 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 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 & ( 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 :Def5: :: 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 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 & 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

proof end;

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 :Def6: :: TSP_2:def 6
for x being Point of X ex a being Point of X st
( a in M & 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 & M /\ (MaxADSet x) = {a} ) )

proof end;

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

begin

definition

let Y be non empty TopStruct ;
let IT be SubSpace of Y;
attr IT 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 )

proof end;

Lm1: now

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 9;
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 V49() SubSpace of Y;
coherence
for b₁ being non empty SubSpace of Y st b₁ is maximal_T_0 holds
b₁ is T_0

proof end;

cluster non empty V49() -> non empty non maximal_T_0 SubSpace of Y;
coherence
for b₁ being non empty SubSpace of Y st not b₁ is T_0 holds
not b₁ 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 T_0 & ( for Y0 being non empty V49() 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 T_0 & ( for Y0 being non empty V49() 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 T_0 & ( for Y0 being non empty V49() 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 SubSpace of X;
coherence
for b₁ being SubSpace of X st b₁ is maximal_T_0 holds
b₁ is dense

proof end;

cluster non dense -> non maximal_T_0 SubSpace of X;
coherence
for b₁ being SubSpace of X st not b₁ is dense holds
not b₁ is maximal_T_0 ;
cluster open maximal_T_0 -> non proper SubSpace of X;
coherence
for b₁ being SubSpace of X st b₁ is open & b₁ is maximal_T_0 holds
not b₁ is proper

proof end;

cluster open proper -> non maximal_T_0 SubSpace of X;
coherence
for b₁ being SubSpace of X st b₁ is open & b₁ is proper holds
not b₁ is maximal_T_0 ;
cluster proper maximal_T_0 -> non open SubSpace of X;
coherence
for b₁ being SubSpace of X st b₁ is proper & b₁ is maximal_T_0 holds
not b₁ is open ;
cluster closed maximal_T_0 -> non proper SubSpace of X;
coherence
for b₁ being SubSpace of X st b₁ is closed & b₁ is maximal_T_0 holds
not b₁ is proper

proof end;

cluster closed proper -> non maximal_T_0 SubSpace of X;
coherence
for b₁ being SubSpace of X st b₁ is closed & b₁ is proper holds
not b₁ is maximal_T_0 ;
cluster proper maximal_T_0 -> non closed SubSpace of X;
coherence
for b₁ being SubSpace of X st b₁ is proper & b₁ is maximal_T_0 holds
not b₁ is closed ;

end;

theorem :: TSP_2:13

for X being non empty TopSpace
for Y0 being non empty V49() 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;
cluster non empty strict TopSpace-like maximal_T_0 SubSpace of X;
existence
ex b₁ being SubSpace of X st
( b₁ is maximal_T_0 & b₁ is strict & not b₁ is empty )

proof end;

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 & G0 = (MaxADSet G) /\ 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 = (MaxADSet F) /\ 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;

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 & ( for a being Point of X holds M /\ (MaxADSet a) = {(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 /\ (MaxADSet a) = {(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 /\ (MaxADSet 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 b₁ being continuous Function of X,X0 st b₁ is being_a_retraction by Th22;
uniqueness
for b₁, b₂ being continuous Function of X,X0 st b₁ is being_a_retraction & b₂ is being_a_retraction holds
b₁ = b₂

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 b₃ being continuous Function of X,X0 holds
( b₃ = Stone-retraction (X,X0) iff b₃ 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}

proof end;

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

proof end;

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

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 :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 b₁ being continuous Function of X,X0 holds
( b₁ = 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) = {(b₁ . 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 b₃ being continuous Function of X,X0 holds
( b₃ = 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) = {(b₃ . 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 b₁ being continuous Function of X,X0 holds
( b₁ = Stone-retraction (X,X0) iff for a being Point of X holds b₁ . 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 b₃ being continuous Function of X,X0 holds
( b₃ = Stone-retraction (X,X0) iff for a being Point of X holds b₃ . 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)) .: (MaxADSet a)

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 /\ (MaxADSet A) = it .: A;
compatibility
for b₁ being continuous Function of X,X0 holds
( b₁ = 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) = b₁ .: 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 b₃ being continuous Function of X,X0 holds
( b₃ = 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) = b₃ .: 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)) .: (MaxADSet A)

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;