:: TSP_1 semantic presentation

definition

let c₁ be TopStruct ;
redefine mode SubSpace as SubSpace of c₁ -> TopStruct means :Def1: :: TSP_1:def 1
( the carrier of a₂ c= the carrier of a₁ & ( for b₁ being Subset of a₂ holds
( b₁ is open iff ex b₂ being Subset of a₁ st
( b₂ is open & b₁ = b₂ /\ the carrier of a₂ ) ) ) );
compatibility

proof end;

coherence ;

end;

:: deftheorem Def1 defines SubSpace TSP_1:def 1 :

theorem Th1: :: TSP_1:1

canceled;

theorem Th2: :: TSP_1:2

for b₁ being TopStruct
for b₂ being SubSpace of b₁
for b₃ being Subset of b₁ st b₃ is open holds
ex b₄ being Subset of b₂ st
( b₄ is open & b₄ = b₃ /\ the carrier of b₂ )

proof end;

definition

let c₁ be TopStruct ;
redefine mode SubSpace as SubSpace of c₁ -> TopStruct means :Def2: :: TSP_1:def 2
( the carrier of a₂ c= the carrier of a₁ & ( for b₁ being Subset of a₂ holds
( b₁ is closed iff ex b₂ being Subset of a₁ st
( b₂ is closed & b₁ = b₂ /\ the carrier of a₂ ) ) ) );
compatibility

proof end;

coherence ;

end;

:: deftheorem Def2 defines SubSpace TSP_1:def 2 :

theorem Th3: :: TSP_1:3

canceled;

theorem Th4: :: TSP_1:4

for b₁ being TopStruct
for b₂ being SubSpace of b₁
for b₃ being Subset of b₁ st b₃ is closed holds
ex b₄ being Subset of b₂ st
( b₄ is closed & b₄ = b₃ /\ the carrier of b₂ )

proof end;

notation

let c₁ be TopStruct ;
synonym T_0 c₁ for discerning c₁;

end;

definition

let c₁ be TopStruct ;
redefine attr a₁ is discerning means :Def3: :: TSP_1:def 3
( a₁ is empty or for b₁, b₂ being Point of a₁ holds
( not b₁ <> b₂ or ex b₃ being Subset of a₁ st
( b₃ is open & b₁ in b₃ & not b₂ in b₃ ) or ex b₃ being Subset of a₁ st
( b₃ is open & not b₁ in b₃ & b₂ in b₃ ) ) );
compatibility

proof end;

end;

:: deftheorem Def3 defines T_0 TSP_1:def 3 :

definition

let c₁ be TopStruct ;
redefine attr a₁ is discerning means :Def4: :: TSP_1:def 4
( a₁ is empty or for b₁, b₂ being Point of a₁ holds
( not b₁ <> b₂ or ex b₃ being Subset of a₁ st
( b₃ is closed & b₁ in b₃ & not b₂ in b₃ ) or ex b₃ being Subset of a₁ st
( b₃ is closed & not b₁ in b₃ & b₂ in b₃ ) ) );
compatibility

proof end;

end;

:: deftheorem Def4 defines T_0 TSP_1:def 4 :

registration

cluster non empty trivial -> non empty T_0 TopStruct ;
coherence

proof end;

cluster non empty non T_0 -> non empty non trivial TopStruct ;
coherence

proof end;

end;

Lemma7: for b₁ being non empty non trivial anti-discrete TopStruct holds not b₁ is T_0

proof end;

registration

cluster non empty strict T_0 TopStruct ;
existence

proof end;

cluster non empty non trivial strict non T_0 TopStruct ;
existence

proof end;

end;

registration

cluster non empty discrete -> non empty T_0 TopStruct ;
coherence

proof end;

cluster non empty non T_0 -> non empty non discrete TopStruct ;
coherence

proof end;

cluster non empty non trivial anti-discrete -> non empty non trivial non T_0 TopStruct ;
coherence by Lemma7;
cluster non empty anti-discrete T_0 -> non empty trivial T_0 TopStruct ;
coherence by Lemma7;
cluster non empty non trivial T_0 -> non empty non anti-discrete TopStruct ;
coherence by Lemma7;

end;

Lemma8: for b₁ being non empty TopSpace
for b₂ being Point of b₁ holds b₂ in Cl {b₂}

proof end;

Lemma9: for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₃ c= Cl b₂ holds
Cl b₃ c= Cl b₂
by TOPS_1:31;

definition

let c₁ be non empty TopSpace;
redefine attr a₁ is discerning means :Def5: :: TSP_1:def 5
for b₁, b₂ being Point of a₁ st b₁ <> b₂ holds
Cl {b₁} <> Cl {b₂};
compatibility

proof end;

end;

:: deftheorem Def5 defines T_0 TSP_1:def 5 :

definition

let c₁ be non empty TopSpace;
redefine attr a₁ is discerning means :Def6: :: TSP_1:def 6
for b₁, b₂ being Point of a₁ holds
( not b₁ <> b₂ or not b₁ in Cl {b₂} or not b₂ in Cl {b₁} );
compatibility

proof end;

end;

:: deftheorem Def6 defines T_0 TSP_1:def 6 :

definition

let c₁ be non empty TopSpace;
redefine attr a₁ is discerning means :: TSP_1:def 7
for b₁, b₂ being Point of a₁ st b₁ <> b₂ & b₁ in Cl {b₂} holds
not Cl {b₂} c= Cl {b₁};
compatibility

proof end;

end;

:: deftheorem Def7 defines T_0 TSP_1:def 7 :

registration

cluster non empty almost_discrete T_0 -> non empty discrete T_0 TopStruct ;
coherence

proof end;

cluster non empty non discrete almost_discrete -> non empty non discrete non T_0 TopStruct ;
coherence

proof end;

cluster non empty non discrete T_0 -> non empty non almost_discrete TopStruct ;
coherence

proof end;

end;

definition

mode Kolmogorov_space is non empty T_0 TopSpace;
mode non-Kolmogorov_space is non empty non T_0 TopSpace;

end;

registration

cluster non trivial strict non anti-discrete TopStruct ;
existence

proof end;

cluster non trivial strict TopStruct ;
existence

proof end;

end;

definition

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
attr a₂ is T_0 means :Def8: :: TSP_1:def 8
for b₁, b₂ being Point of a₁ st b₁ in a₂ & b₂ in a₂ & b₁ <> b₂ & ( for b₃ being Subset of a₁ holds
( not b₃ is open or not b₁ in b₃ or b₂ in b₃ ) ) holds
ex b₃ being Subset of a₁ st
( b₃ is open & not b₁ in b₃ & b₂ in b₃ );

end;

:: deftheorem Def8 defines T_0 TSP_1:def 8 :

definition

let c₁ be non empty TopStruct ;
let c₂ be Subset of c₁;
redefine attr a₂ is T_0 means :Def9: :: TSP_1:def 9
for b₁, b₂ being Point of a₁ st b₁ in a₂ & b₂ in a₂ & b₁ <> b₂ & ( for b₃ being Subset of a₁ holds
( not b₃ is closed or not b₁ in b₃ or b₂ in b₃ ) ) holds
ex b₃ being Subset of a₁ st
( b₃ is closed & not b₁ in b₃ & b₂ in b₃ );
compatibility

proof end;

end;

:: deftheorem Def9 defines T_0 TSP_1:def 9 :

theorem Th5: :: TSP_1:5

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 T_0 holds
b₄ is T_0

proof end;

theorem Th6: :: TSP_1:6

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

proof end;

theorem Th7: :: TSP_1:7

for b₁ being non empty TopStruct
for b₂, b₃ being Subset of b₁ st b₃ c= b₂ & b₂ is T_0 holds
b₃ is T_0

proof end;

theorem Th8: :: TSP_1:8

for b₁ being non empty TopStruct
for b₂, b₃ being Subset of b₁ st ( b₂ is T_0 or b₃ is T_0 ) holds
b₂ /\ b₃ is T_0

proof end;

theorem Th9: :: TSP_1:9

for b₁ being non empty TopStruct
for b₂, b₃ being Subset of b₁ st ( b₂ is open or b₃ is open ) & b₂ is T_0 & b₃ is T_0 holds
b₂ \/ b₃ is T_0

proof end;

theorem Th10: :: TSP_1:10

for b₁ being non empty TopStruct
for b₂, b₃ being Subset of b₁ st ( b₂ is closed or b₃ is closed ) & b₂ is T_0 & b₃ is T_0 holds
b₂ \/ b₃ is T_0

proof end;

theorem Th11: :: TSP_1:11

for b₁ being non empty TopStruct
for b₂ being Subset of b₁ st b₂ is discrete holds
b₂ is T_0

proof end;

theorem Th12: :: TSP_1:12

for b₁ being non empty TopStruct
for b₂ being non empty Subset of b₁ st b₂ is anti-discrete & not b₂ is trivial holds
not b₂ is T_0

proof end;

definition

let c₁ be non empty TopSpace;
let c₂ be Subset of c₁;
redefine attr a₂ is T_0 means :Def10: :: TSP_1:def 10
for b₁, b₂ being Point of a₁ st b₁ in a₂ & b₂ in a₂ & b₁ <> b₂ holds
Cl {b₁} <> Cl {b₂};
compatibility

proof end;

end;

:: deftheorem Def10 defines T_0 TSP_1:def 10 :

definition

let c₁ be non empty TopSpace;
let c₂ be Subset of c₁;
redefine attr a₂ is T_0 means :Def11: :: TSP_1:def 11
for b₁, b₂ being Point of a₁ st b₁ in a₂ & b₂ in a₂ & b₁ <> b₂ & b₁ in Cl {b₂} holds
not b₂ in Cl {b₁};
compatibility

proof end;

end;

:: deftheorem Def11 defines T_0 TSP_1:def 11 :

definition

let c₁ be non empty TopSpace;
let c₂ be Subset of c₁;
redefine attr a₂ is T_0 means :: TSP_1:def 12
for b₁, b₂ being Point of a₁ st b₁ in a₂ & b₂ in a₂ & b₁ <> b₂ & b₁ in Cl {b₂} holds
not Cl {b₂} c= Cl {b₁};
compatibility

proof end;

end;

:: deftheorem Def12 defines T_0 TSP_1:def 12 :

theorem Th13: :: TSP_1:13

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

proof end;

theorem Th14: :: TSP_1:14

for b₁ being non empty TopSpace
for b₂ being Point of b₁ holds {b₂} is T_0

proof end;

registration

let c₁ be non empty TopStruct ;
cluster non empty strict T_0 SubSpace of a₁;
existence

proof end;

end;

E23: now

let c₁ be 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;

definition

let c₁ be TopStruct ;
let c₂ be SubSpace of c₁;
redefine attr T_0 as a₂ is T_0 means :: TSP_1:def 13
( a₂ is empty or for b₁, b₂ being Point of a₁ st b₁ is Point of a₂ & b₂ is Point of a₂ & b₁ <> b₂ & ( for b₃ being Subset of a₁ holds
( not b₃ is open or not b₁ in b₃ or b₂ in b₃ ) ) holds
ex b₃ being Subset of a₁ st
( b₃ is open & not b₁ in b₃ & b₂ in b₃ ) );
compatibility

proof end;

end;

:: deftheorem Def13 defines T_0 TSP_1:def 13 :

definition

let c₁ be TopStruct ;
let c₂ be SubSpace of c₁;
redefine attr T_0 as a₂ is T_0 means :Def14: :: TSP_1:def 14
( a₂ is empty or for b₁, b₂ being Point of a₁ st b₁ is Point of a₂ & b₂ is Point of a₂ & b₁ <> b₂ & ( for b₃ being Subset of a₁ holds
( not b₃ is closed or not b₁ in b₃ or b₂ in b₃ ) ) holds
ex b₃ being Subset of a₁ st
( b₃ is closed & not b₁ in b₃ & b₂ in b₃ ) );
compatibility

proof end;

end;

:: deftheorem Def14 defines T_0 TSP_1:def 14 :

theorem Th15: :: TSP_1:15

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

proof end;

theorem Th16: :: TSP_1:16

for b₁ being non empty TopStruct
for b₂ being non empty SubSpace of b₁
for b₃ being non empty V91 SubSpace of b₁ st b₂ is SubSpace of b₃ holds
b₂ is T_0

proof end;

theorem Th17: :: TSP_1:17

for b₁ being non empty TopSpace
for b₂ being non empty V91 SubSpace of b₁
for b₃ being non empty SubSpace of b₁ st b₂ meets b₃ holds
b₂ meet b₃ is T_0

proof end;

theorem Th18: :: TSP_1:18

for b₁ being non empty TopSpace
for b₂, b₃ being non empty V91 SubSpace of b₁ st ( b₂ is open or b₃ is open ) holds
b₂ union b₃ is T_0

proof end;

theorem Th19: :: TSP_1:19

for b₁ being non empty TopSpace
for b₂, b₃ being non empty V91 SubSpace of b₁ st ( b₂ is closed or b₃ is closed ) holds
b₂ union b₃ is T_0

proof end;

definition

let c₁ be non empty TopSpace;
mode Kolmogorov_subspace of a₁ is non empty V91 SubSpace of a₁;

end;

theorem Th20: :: TSP_1:20

for b₁ being non empty TopSpace
for b₂ being non empty Subset of b₁ st b₂ is T_0 holds
ex b₃ being strict Kolmogorov_subspace of b₁ st b₂ = the carrier of b₃

proof end;

registration

let c₁ be non empty non trivial TopSpace;
cluster strict proper SubSpace of a₁;
existence

proof end;

end;

registration

let c₁ be Kolmogorov_space;
cluster non empty -> non empty V91 SubSpace of a₁;
coherence

proof end;

end;

registration

let c₁ be non-Kolmogorov_space;
cluster non empty non proper -> non empty non trivial V91 SubSpace of a₁;
coherence

proof end;

cluster non empty V91 -> non empty proper SubSpace of a₁;
coherence

proof end;

end;

registration

let c₁ be non-Kolmogorov_space;
cluster strict V91 SubSpace of a₁;
existence

proof end;

end;

definition

let c₁ be non-Kolmogorov_space;
mode non-Kolmogorov_subspace of a₁ is V91 SubSpace of a₁;

end;

theorem Th21: :: TSP_1:21

for b₁ being non empty non-Kolmogorov_space
for b₂ being Subset of b₁ st not b₂ is T_0 holds
ex b₃ being strict non-Kolmogorov_subspace of b₁ st b₂ = the carrier of b₃

proof end;