:: TSP_2 semantic presentation

definition

let c₁ be non empty TopSpace;
let c₂ be Subset of c₁;
redefine attr a₂ is T_0 means :Def1: :: TSP_2:def 1
for b₁, b₂ being Point of a₁ st b₁ in a₂ & b₂ in a₂ & b₁ <> b₂ holds
MaxADSet b₁ misses MaxADSet b₂;
compatibility

proof end;

end;

:: deftheorem Def1 defines T_0 TSP_2:def 1 :

definition

let c₁ be non empty TopSpace;
let c₂ be Subset of c₁;
redefine attr a₂ is T_0 means :Def2: :: TSP_2:def 2
for b₁ being Point of a₁ st b₁ in a₂ holds
a₂ /\ (MaxADSet b₁) = {b₁};
compatibility

proof end;

end;

:: deftheorem Def2 defines T_0 TSP_2:def 2 :

definition

let c₁ be non empty TopSpace;
let c₂ be Subset of c₁;
redefine attr a₂ is T_0 means :: TSP_2:def 3
for b₁ being Point of a₁ st b₁ in a₂ holds
ex b₂ being Subset of a₁ st
( b₂ is maximal_anti-discrete & a₂ /\ b₂ = {b₁} );
compatibility

proof end;

end;

:: deftheorem Def3 defines T_0 TSP_2:def 3 :

definition

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
attr a₂ is maximal_T_0 means :Def4: :: TSP_2:def 4
( a₂ is T_0 & ( for b₁ being Subset of a₁ st b₁ is T_0 & a₂ c= b₁ holds
a₂ = b₁ ) );

end;

:: deftheorem Def4 defines maximal_T_0 TSP_2:def 4 :

theorem Th1: :: TSP_2:1

for b₁, b₂ being TopStruct
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st TopStruct(# the carrier of b₁,the topology of b₁ #) = TopStruct(# the carrier of b₂,the topology of b₂ #) & b₃ = b₄ & b₃ is maximal_T_0 holds
b₄ is maximal_T_0

proof end;

definition

let c₁ be non empty TopSpace;
let c₂ be Subset of c₁;
redefine attr a₂ is maximal_T_0 means :Def5: :: TSP_2:def 5
( a₂ is T_0 & MaxADSet a₂ = the carrier of a₁ );
compatibility

proof end;

end;

:: deftheorem Def5 defines maximal_T_0 TSP_2:def 5 :

theorem Th2: :: TSP_2:2

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ is maximal_T_0 holds
b₂ is dense

proof end;

theorem Th3: :: TSP_2:3

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st ( b₂ is open or b₂ is closed ) & b₂ is maximal_T_0 holds
not b₂ is proper

proof end;

theorem Th4: :: TSP_2:4

for b₁ being non empty TopSpace
for b₂ being empty Subset of b₁ holds not b₂ is maximal_T_0

proof end;

theorem Th5: :: TSP_2:5

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ is maximal_T_0 holds
for b₃ being Subset of b₁ st b₃ is closed holds
b₃ = MaxADSet (b₂ /\ b₃)

proof end;

theorem Th6: :: TSP_2:6

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ is maximal_T_0 holds
for b₃ being Subset of b₁ st b₃ is open holds
b₃ = MaxADSet (b₂ /\ b₃)

proof end;

theorem Th7: :: TSP_2:7

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ is maximal_T_0 holds
for b₃ being Subset of b₁ holds Cl b₃ = MaxADSet (b₂ /\ (Cl b₃)) by Th5;

theorem Th8: :: TSP_2:8

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ is maximal_T_0 holds
for b₃ being Subset of b₁ holds Int b₃ = MaxADSet (b₂ /\ (Int b₃)) by Th6;

definition

let c₁ be non empty TopSpace;
let c₂ be Subset of c₁;
redefine attr a₂ is maximal_T_0 means :Def6: :: TSP_2:def 6
for b₁ being Point of a₁ ex b₂ being Point of a₁ st
( b₂ in a₂ & a₂ /\ (MaxADSet b₁) = {b₂} );
compatibility

proof end;

end;

:: deftheorem Def6 defines maximal_T_0 TSP_2:def 6 :

theorem Th9: :: TSP_2:9

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ is T_0 holds
ex b₃ being Subset of b₁ st
( b₂ c= b₃ & b₃ is maximal_T_0 )

proof end;

theorem Th10: :: TSP_2:10

for b₁ being non empty TopSpace ex b₂ being Subset of b₁ st b₂ is maximal_T_0

proof end;

definition

let c₁ be non empty TopStruct ;
let c₂ be SubSpace of c₁;
attr a₂ is maximal_T_0 means :Def7: :: TSP_2:def 7
for b₁ being Subset of a₁ st b₁ = the carrier of a₂ holds
b₁ is maximal_T_0;

end;

:: deftheorem Def7 defines maximal_T_0 TSP_2:def 7 :

theorem Th11: :: TSP_2:11

for b₁ being non empty TopStruct
for b₂ being SubSpace of b₁
for b₃ being Subset of b₁ st b₃ = the carrier of b₂ holds
( b₃ is maximal_T_0 iff b₂ is maximal_T_0 )

proof end;

E15: now

let c₁ be non empty TopStruct ;
let c₂ be SubSpace of c₁;
( [#] c₂ c= [#] c₁ & [#] c₂ = the carrier of c₂ ) by PRE_TOPC:12, PRE_TOPC:def 9;
hence the carrier of c₂ is Subset of c₁ by PRE_TOPC:12;

end;

registration

let c₁ be non empty TopStruct ;
cluster non empty maximal_T_0 -> non empty V48 SubSpace of a₁;
coherence

proof end;

cluster non empty V48 -> non empty non maximal_T_0 SubSpace of a₁;
coherence

proof end;

end;

definition

let c₁ be non empty TopSpace;
let c₂ be non empty SubSpace of c₁;
redefine attr a₂ is maximal_T_0 means :: TSP_2:def 8
( a₂ is T_0 & ( for b₁ being non empty V48 SubSpace of a₁ st a₂ is SubSpace of b₁ holds
TopStruct(# the carrier of a₂,the topology of a₂ #) = TopStruct(# the carrier of b₁,the topology of b₁ #) ) );
compatibility

proof end;

end;

:: deftheorem Def8 defines maximal_T_0 TSP_2:def 8 :

theorem Th12: :: TSP_2:12

for b₁ being non empty TopSpace
for b₂ being non empty Subset of b₁ st b₂ is maximal_T_0 holds
ex b₃ being non empty strict SubSpace of b₁ st
( b₃ is maximal_T_0 & b₂ = the carrier of b₃ )

proof end;

registration

let c₁ be non empty TopSpace;
cluster maximal_T_0 -> dense SubSpace of a₁;
coherence

proof end;

cluster non dense -> non maximal_T_0 SubSpace of a₁;
coherence

proof end;

cluster open maximal_T_0 -> non proper SubSpace of a₁;
coherence

proof end;

cluster open proper -> non maximal_T_0 SubSpace of a₁;
coherence

proof end;

cluster proper maximal_T_0 -> non open SubSpace of a₁;
coherence

proof end;

cluster closed maximal_T_0 -> non proper SubSpace of a₁;
coherence

proof end;

cluster proper closed -> non maximal_T_0 SubSpace of a₁;
coherence

proof end;

cluster proper maximal_T_0 -> non closed SubSpace of a₁;
coherence

proof end;

end;

theorem Th13: :: TSP_2:13

for b₁ being non empty TopSpace
for b₂ being non empty V48 SubSpace of b₁ ex b₃ being strict SubSpace of b₁ st
( b₂ is SubSpace of b₃ & b₃ is maximal_T_0 )

proof end;

registration

let c₁ be non empty TopSpace;
cluster non empty strict dense V48 maximal_T_0 SubSpace of a₁;
existence

proof end;

end;

definition

let c₁ be non empty TopSpace;
mode maximal_Kolmogorov_subspace of a₁ is maximal_T_0 SubSpace of a₁;

end;

theorem Th14: :: TSP_2:14

for b₁ being non empty TopSpace
for b₂ being maximal_Kolmogorov_subspace of b₁
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st b₄ = b₃ holds
( b₄ is open iff ( MaxADSet b₃ is open & b₄ = (MaxADSet b₃) /\ the carrier of b₂ ) )

proof end;

theorem Th15: :: TSP_2:15

for b₁ being non empty TopSpace
for b₂ being maximal_Kolmogorov_subspace of b₁
for b₃ being Subset of b₁ holds
( b₃ is open iff ( b₃ = MaxADSet b₃ & ex b₄ being Subset of b₂ st
( b₄ is open & b₄ = b₃ /\ the carrier of b₂ ) ) )

proof end;

theorem Th16: :: TSP_2:16

for b₁ being non empty TopSpace
for b₂ being maximal_Kolmogorov_subspace of b₁
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st b₄ = b₃ holds
( b₄ is closed iff ( MaxADSet b₃ is closed & b₄ = (MaxADSet b₃) /\ the carrier of b₂ ) )

proof end;

theorem Th17: :: TSP_2:17

for b₁ being non empty TopSpace
for b₂ being maximal_Kolmogorov_subspace of b₁
for b₃ being Subset of b₁ holds
( b₃ is closed iff ( b₃ = MaxADSet b₃ & ex b₄ being Subset of b₂ st
( b₄ is closed & b₄ = b₃ /\ the carrier of b₂ ) ) )

proof end;

theorem Th18: :: TSP_2:18

for b₁ being non empty TopSpace
for b₂ being non empty maximal_Kolmogorov_subspace of b₁
for b₃ being Function of b₁,b₂
for b₄ being Subset of b₁ st b₄ = the carrier of b₂ & ( for b₅ being Point of b₁ holds b₄ /\ (MaxADSet b₅) = {(b₃ . b₅)} ) holds
b₃ is continuous Function of b₁,b₂

proof end;

theorem Th19: :: TSP_2:19

for b₁ being non empty TopSpace
for b₂ being non empty maximal_Kolmogorov_subspace of b₁
for b₃ being Function of b₁,b₂ st ( for b₄ being Point of b₁ holds b₃ . b₄ in MaxADSet b₄ ) holds
b₃ is continuous Function of b₁,b₂

proof end;

theorem Th20: :: TSP_2:20

for b₁ being non empty TopSpace
for b₂ being non empty maximal_Kolmogorov_subspace of b₁
for b₃ being continuous Function of b₁,b₂
for b₄ being Subset of b₁ st b₄ = the carrier of b₂ & ( for b₅ being Point of b₁ holds b₄ /\ (MaxADSet b₅) = {(b₃ . b₅)} ) holds
b₃ is_a_retraction

proof end;

theorem Th21: :: TSP_2:21

for b₁ being non empty TopSpace
for b₂ being non empty maximal_Kolmogorov_subspace of b₁
for b₃ being continuous Function of b₁,b₂ st ( for b₄ being Point of b₁ holds b₃ . b₄ in MaxADSet b₄ ) holds
b₃ is_a_retraction

proof end;

theorem Th22: :: TSP_2:22

for b₁ being non empty TopSpace
for b₂ being non empty maximal_Kolmogorov_subspace of b₁ ex b₃ being continuous Function of b₁,b₂ st b₃ is_a_retraction

proof end;

theorem Th23: :: TSP_2:23

for b₁ being non empty TopSpace
for b₂ being non empty maximal_Kolmogorov_subspace of b₁ holds b₂ is_a_retract_of b₁

proof end;

Lemma23: for b₁ being non empty TopSpace
for b₂ being non empty maximal_Kolmogorov_subspace of b₁
for b₃ being continuous Function of b₁,b₂ st b₃ is_a_retraction holds
for b₄ being Point of b₁
for b₅ being Point of b₂ st b₄ = b₅ holds
b₃ " (Cl {b₅}) = Cl {b₄}

proof end;

Lemma24: for b₁ being non empty TopSpace
for b₂ being non empty maximal_Kolmogorov_subspace of b₁
for b₃ being continuous Function of b₁,b₂ st b₃ is_a_retraction holds
for b₄ being Subset of b₁ st b₄ = the carrier of b₂ holds
for b₅ being Point of b₁ holds b₄ /\ (MaxADSet b₅) = {(b₃ . b₅)}

proof end;

Lemma25: for b₁ being non empty TopSpace
for b₂ being non empty maximal_Kolmogorov_subspace of b₁
for b₃ being continuous Function of b₁,b₂ st b₃ is_a_retraction holds
for b₄ being Point of b₁
for b₅ being Point of b₂ st b₄ = b₅ holds
MaxADSet b₄ c= b₃ " {b₅}

proof end;

Lemma26: for b₁ being non empty TopSpace
for b₂ being non empty maximal_Kolmogorov_subspace of b₁
for b₃ being continuous Function of b₁,b₂ st b₃ is_a_retraction holds
for b₄ being Point of b₁
for b₅ being Point of b₂ st b₄ = b₅ holds
b₃ " {b₅} = MaxADSet b₄

proof end;

Lemma27: for b₁ being non empty TopSpace
for b₂ being non empty maximal_Kolmogorov_subspace of b₁
for b₃ being continuous Function of b₁,b₂ st b₃ is_a_retraction holds
for b₄ being Subset of b₁
for b₅ being Subset of b₂ st b₅ = b₄ holds
b₃ " b₅ = MaxADSet b₄

proof end;

definition

let c₁ be non empty TopSpace;
let c₂ be non empty maximal_Kolmogorov_subspace of c₁;
func Stone-retraction c₁,c₂ -> continuous Function of a₁,a₂ means :Def9: :: TSP_2:def 9
a₃ is_a_retraction ;
existence by Th22;
uniqueness

proof end;

end;

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

theorem Th24: :: TSP_2:24

for b₁ being non empty TopSpace
for b₂ being non empty maximal_Kolmogorov_subspace of b₁
for b₃ being Point of b₁
for b₄ being Point of b₂ st b₃ = b₄ holds
(Stone-retraction b₁,b₂) " (Cl {b₄}) = Cl {b₃}

proof end;

theorem Th25: :: TSP_2:25

for b₁ being non empty TopSpace
for b₂ being non empty maximal_Kolmogorov_subspace of b₁
for b₃ being Point of b₁
for b₄ being Point of b₂ st b₃ = b₄ holds
(Stone-retraction b₁,b₂) " {b₄} = MaxADSet b₃

proof end;

theorem Th26: :: TSP_2:26

for b₁ being non empty TopSpace
for b₂ being non empty maximal_Kolmogorov_subspace of b₁
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st b₄ = b₃ holds
(Stone-retraction b₁,b₂) " b₄ = MaxADSet b₃

proof end;

definition

let c₁ be non empty TopSpace;
let c₂ be non empty maximal_Kolmogorov_subspace of c₁;
redefine func Stone-retraction as Stone-retraction c₁,c₂ -> continuous Function of a₁,a₂ means :Def10: :: TSP_2:def 10
for b₁ being Subset of a₁ st b₁ = the carrier of a₂ holds
for b₂ being Point of a₁ holds b₁ /\ (MaxADSet b₂) = {(a₃ . b₂)};
compatibility

proof end;

coherence ;

end;

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

definition

let c₁ be non empty TopSpace;
let c₂ be non empty maximal_Kolmogorov_subspace of c₁;
redefine func Stone-retraction as Stone-retraction c₁,c₂ -> continuous Function of a₁,a₂ means :Def11: :: TSP_2:def 11
for b₁ being Point of a₁ holds a₃ . b₁ in MaxADSet b₁;
compatibility

proof end;

coherence ;

end;

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

theorem Th27: :: TSP_2:27

for b₁ being non empty TopSpace
for b₂ being non empty maximal_Kolmogorov_subspace of b₁
for b₃ being Point of b₁ holds (Stone-retraction b₁,b₂) " {((Stone-retraction b₁,b₂) . b₃)} = MaxADSet b₃

proof end;

theorem Th28: :: TSP_2:28

for b₁ being non empty TopSpace
for b₂ being non empty maximal_Kolmogorov_subspace of b₁
for b₃ being Point of b₁ holds (Stone-retraction b₁,b₂) .: {b₃} = (Stone-retraction b₁,b₂) .: (MaxADSet b₃)

proof end;

definition

let c₁ be non empty TopSpace;
let c₂ be non empty maximal_Kolmogorov_subspace of c₁;
redefine func Stone-retraction as Stone-retraction c₁,c₂ -> continuous Function of a₁,a₂ means :Def12: :: TSP_2:def 12
for b₁ being Subset of a₁ st b₁ = the carrier of a₂ holds
for b₂ being Subset of a₁ holds b₁ /\ (MaxADSet b₂) = a₃ .: b₂;
compatibility

proof end;

coherence ;

end;

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

theorem Th29: :: TSP_2:29

for b₁ being non empty TopSpace
for b₂ being non empty maximal_Kolmogorov_subspace of b₁
for b₃ being Subset of b₁ holds (Stone-retraction b₁,b₂) " ((Stone-retraction b₁,b₂) .: b₃) = MaxADSet b₃

proof end;

theorem Th30: :: TSP_2:30

for b₁ being non empty TopSpace
for b₂ being non empty maximal_Kolmogorov_subspace of b₁
for b₃ being Subset of b₁ holds (Stone-retraction b₁,b₂) .: b₃ = (Stone-retraction b₁,b₂) .: (MaxADSet b₃)

proof end;

theorem Th31: :: TSP_2:31

for b₁ being non empty TopSpace
for b₂ being non empty maximal_Kolmogorov_subspace of b₁
for b₃, b₄ being Subset of b₁ holds (Stone-retraction b₁,b₂) .: (b₃ \/ b₄) = ((Stone-retraction b₁,b₂) .: b₃) \/ ((Stone-retraction b₁,b₂) .: b₄)

proof end;

theorem Th32: :: TSP_2:32

for b₁ being non empty TopSpace
for b₂ being non empty maximal_Kolmogorov_subspace of b₁
for b₃, b₄ being Subset of b₁ st ( b₃ is open or b₄ is open ) holds
(Stone-retraction b₁,b₂) .: (b₃ /\ b₄) = ((Stone-retraction b₁,b₂) .: b₃) /\ ((Stone-retraction b₁,b₂) .: b₄)

proof end;

theorem Th33: :: TSP_2:33

for b₁ being non empty TopSpace
for b₂ being non empty maximal_Kolmogorov_subspace of b₁
for b₃, b₄ being Subset of b₁ st ( b₃ is closed or b₄ is closed ) holds
(Stone-retraction b₁,b₂) .: (b₃ /\ b₄) = ((Stone-retraction b₁,b₂) .: b₃) /\ ((Stone-retraction b₁,b₂) .: b₄)

proof end;

theorem Th34: :: TSP_2:34

for b₁ being non empty TopSpace
for b₂ being non empty maximal_Kolmogorov_subspace of b₁
for b₃ being Subset of b₁ st b₃ is open holds
(Stone-retraction b₁,b₂) .: b₃ is open

proof end;

theorem Th35: :: TSP_2:35

for b₁ being non empty TopSpace
for b₂ being non empty maximal_Kolmogorov_subspace of b₁
for b₃ being Subset of b₁ st b₃ is closed holds
(Stone-retraction b₁,b₂) .: b₃ is closed

proof end;