:: TSP_2 semantic presentation

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

proof end;

end;

:: deftheorem Def1 defines T_0 TSP_2:def 1 :

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

proof end;

end;

:: deftheorem Def2 defines T_0 TSP_2:def 2 :

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

proof end;

end;

:: deftheorem defines T_0 TSP_2:def 3 :

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 :

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

proof end;

end;

:: deftheorem Def5 defines maximal_T_0 TSP_2:def 5 :

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

proof end;

end;

:: deftheorem Def6 defines maximal_T_0 TSP_2:def 6 :

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;

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 :

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:
let Z0 be SubSpace of Z; :: thesis:
( [#] Z0 c= [#] Z & [#] Z0 = the carrier of Z0 ) by PRE_TOPC:12, PRE_TOPC:def 9;
hence the carrier of Z0 is Subset of Z by PRE_TOPC:12; :: thesis:

end;

registration

let Y be non empty TopStruct ;
cluster non empty maximal_T_0 -> non empty V48 SubSpace of Y;
coherence

proof end;

cluster non empty V48 -> non empty non maximal_T_0 SubSpace of Y;
coherence

proof end;

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 V48 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

proof end;

end;

:: deftheorem defines maximal_T_0 TSP_2:def 8 :

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

proof end;

cluster non dense -> non maximal_T_0 SubSpace of X;
coherence

proof end;

cluster open maximal_T_0 -> non proper SubSpace of X;
coherence

proof end;

cluster open proper -> non maximal_T_0 SubSpace of X;
coherence

proof end;

cluster proper maximal_T_0 -> non open SubSpace of X;
coherence

proof end;

cluster closed maximal_T_0 -> non proper SubSpace of X;
coherence

proof end;

cluster proper closed -> non maximal_T_0 SubSpace of X;
coherence

proof end;

cluster proper maximal_T_0 -> non closed SubSpace of X;
coherence

proof end;

end;

theorem :: TSP_2:13

for X being non empty TopSpace
for Y0 being non empty V48 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 dense V48 maximal_T_0 SubSpace of X;
existence

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;

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_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_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_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_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_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_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_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_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_a_retraction ;
existence by Th22;
uniqueness

proof end;

end;

:: deftheorem Def9 defines Stone-retraction TSP_2:def 9 :

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;
:: original: Stone-retraction
redefine func Stone-retraction X,X0 -> continuous Function of 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

proof end;

coherence ;

end;

:: deftheorem Def10 defines Stone-retraction TSP_2:def 10 :

definition

let X be non empty TopSpace;
let X0 be non empty maximal_Kolmogorov_subspace of X;
:: original: Stone-retraction
redefine func Stone-retraction X,X0 -> continuous Function of X,X0 means :Def11: :: TSP_2:def 11
for a being Point of X holds it . a in MaxADSet a;
compatibility

proof end;

coherence ;

end;

:: deftheorem Def11 defines Stone-retraction TSP_2:def 11 :

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 (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;
:: original: Stone-retraction
redefine func Stone-retraction X,X0 -> continuous Function of 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

proof end;

coherence ;

end;

:: deftheorem Def12 defines Stone-retraction TSP_2:def 12 :

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;