:: TSP_1 semantic presentation

definition

let Y be TopStruct ;
:: original: SubSpace
redefine mode SubSpace of Y -> TopStruct means :Def1: :: TSP_1:def 1
( the carrier of it c= the carrier of Y & ( for G0 being Subset of it holds
( G0 is open iff ex G being Subset of Y st
( G is open & G0 = G /\ the carrier of it ) ) ) );
compatibility

proof end;

coherence ;

end;

:: deftheorem Def1 defines SubSpace TSP_1:def 1 :

theorem :: TSP_1:1

canceled;

theorem Th2: :: TSP_1:2

for Y being TopStruct
for Y0 being SubSpace of Y
for G being Subset of Y st G is open holds
ex G0 being Subset of Y0 st
( G0 is open & G0 = G /\ the carrier of Y0 )

proof end;

definition

let Y be TopStruct ;
:: original: SubSpace
redefine mode SubSpace of Y -> TopStruct means :Def2: :: TSP_1:def 2
( the carrier of it c= the carrier of Y & ( for F0 being Subset of it holds
( F0 is closed iff ex F being Subset of Y st
( F is closed & F0 = F /\ the carrier of it ) ) ) );
compatibility

proof end;

coherence ;

end;

:: deftheorem Def2 defines SubSpace TSP_1:def 2 :

theorem :: TSP_1:3

canceled;

theorem Th4: :: TSP_1:4

for Y being TopStruct
for Y0 being SubSpace of Y
for F being Subset of Y st F is closed holds
ex F0 being Subset of Y0 st
( F0 is closed & F0 = F /\ the carrier of Y0 )

proof end;

notation

let T be TopStruct ;
synonym T_0 T for discerning T;

end;

definition

let T be TopStruct ;
redefine attr T is discerning means :Def3: :: TSP_1:def 3
( T is empty or for x, y being Point of T holds
( not x <> y or ex V being Subset of T st
( V is open & x in V & not y in V ) or ex W being Subset of T st
( W is open & not x in W & y in W ) ) );
compatibility

proof end;

end;

:: deftheorem Def3 defines T_0 TSP_1:def 3 :

definition

let Y be TopStruct ;
redefine attr Y is discerning means :Def4: :: TSP_1:def 4
( Y is empty or for x, y being Point of Y holds
( not x <> y or ex E being Subset of Y st
( E is closed & x in E & not y in E ) or ex F being Subset of Y st
( F is closed & not x in F & y in F ) ) );
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;

Lm1: for X being non empty non trivial anti-discrete TopStruct holds not X 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 Lm1;
cluster non empty anti-discrete T_0 -> non empty trivial T_0 TopStruct ;
coherence by Lm1;
cluster non empty non trivial T_0 -> non empty non anti-discrete TopStruct ;
coherence by Lm1;

end;

Lm2: for X being non empty TopSpace
for x being Point of X holds x in Cl {x}

proof end;

Lm3: for X being non empty TopSpace
for A, B being Subset of X st B c= Cl A holds
Cl B c= Cl A
by TOPS_1:31;

definition

let X be non empty TopSpace;
redefine attr X is discerning means :Def5: :: TSP_1:def 5
for x, y being Point of X st x <> y holds
Cl {x} <> Cl {y};
compatibility

proof end;

end;

:: deftheorem Def5 defines T_0 TSP_1:def 5 :

definition

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

proof end;

end;

:: deftheorem Def6 defines T_0 TSP_1:def 6 :

definition

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

proof end;

end;

:: deftheorem 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 Y be TopStruct ;
let IT be Subset of Y;
attr IT is T_0 means :Def8: :: TSP_1:def 8
for x, y being Point of Y st x in IT & y in IT & x <> y & ( for V being Subset of Y holds
( not V is open or not x in V or y in V ) ) holds
ex W being Subset of Y st
( W is open & not x in W & y in W );

end;

:: deftheorem Def8 defines T_0 TSP_1:def 8 :

definition

let Y be non empty TopStruct ;
let A be Subset of Y;
redefine attr A is T_0 means :Def9: :: TSP_1:def 9
for x, y being Point of Y st x in A & y in A & x <> y & ( for E being Subset of Y holds
( not E is closed or not x in E or y in E ) ) holds
ex F being Subset of Y st
( F is closed & not x in F & y in F );
compatibility

proof end;

end;

:: deftheorem Def9 defines T_0 TSP_1:def 9 :

theorem :: TSP_1:5

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 T_0 holds
D1 is T_0

proof end;

theorem Th6: :: TSP_1:6

for Y being non empty TopStruct
for A being Subset of Y st A = the carrier of Y holds
( A is T_0 iff Y is T_0 )

proof end;

theorem Th7: :: TSP_1:7

for Y being non empty TopStruct
for A, B being Subset of Y st B c= A & A is T_0 holds
B is T_0

proof end;

theorem Th8: :: TSP_1:8

for Y being non empty TopStruct
for A, B being Subset of Y st ( A is T_0 or B is T_0 ) holds
A /\ B is T_0

proof end;

theorem Th9: :: TSP_1:9

for Y being non empty TopStruct
for A, B being Subset of Y st ( A is open or B is open ) & A is T_0 & B is T_0 holds
A \/ B is T_0

proof end;

theorem Th10: :: TSP_1:10

for Y being non empty TopStruct
for A, B being Subset of Y st ( A is closed or B is closed ) & A is T_0 & B is T_0 holds
A \/ B is T_0

proof end;

theorem Th11: :: TSP_1:11

for Y being non empty TopStruct
for A being Subset of Y st A is discrete holds
A is T_0

proof end;

theorem :: TSP_1:12

for Y being non empty TopStruct
for A being non empty Subset of Y st A is anti-discrete & not A is trivial holds
not A is T_0

proof end;

definition

let X be non empty TopSpace;
let A be Subset of X;
redefine attr A is T_0 means :Def10: :: TSP_1:def 10
for x, y being Point of X st x in A & y in A & x <> y holds
Cl {x} <> Cl {y};
compatibility

proof end;

end;

:: deftheorem Def10 defines T_0 TSP_1:def 10 :

definition

let X be non empty TopSpace;
let A be Subset of X;
redefine attr A is T_0 means :Def11: :: TSP_1:def 11
for x, y being Point of X st x in A & y in A & x <> y & x in Cl {y} holds
not y in Cl {x};
compatibility

proof end;

end;

:: deftheorem Def11 defines T_0 TSP_1:def 11 :

definition

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

proof end;

end;

:: deftheorem defines T_0 TSP_1:def 12 :

theorem Th13: :: TSP_1:13

for X being non empty TopSpace
for A being empty Subset of X holds A is T_0

proof end;

theorem :: TSP_1:14

for X being non empty TopSpace
for x being Point of X holds {x} is T_0

proof end;

registration

let Y be non empty TopStruct ;
cluster non empty strict T_0 SubSpace of Y;
existence

proof end;

end;

Lm4: now

let Z be 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;

definition

let Y be TopStruct ;
let Y0 be SubSpace of Y;
:: original: T_0
redefine attr Y0 is T_0 means :: TSP_1:def 13
( Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for V being Subset of Y holds
( not V is open or not x in V or y in V ) ) holds
ex W being Subset of Y st
( W is open & not x in W & y in W ) );
compatibility

proof end;

end;

:: deftheorem defines T_0 TSP_1:def 13 :

definition

let Y be TopStruct ;
let Y0 be SubSpace of Y;
:: original: T_0
redefine attr Y0 is T_0 means :Def14: :: TSP_1:def 14
( Y0 is empty or for x, y being Point of Y st x is Point of Y0 & y is Point of Y0 & x <> y & ( for E being Subset of Y holds
( not E is closed or not x in E or y in E ) ) holds
ex F being Subset of Y st
( F is closed & not x in F & y in F ) );
compatibility

proof end;

end;

:: deftheorem Def14 defines T_0 TSP_1:def 14 :

theorem Th15: :: TSP_1:15

for Y being non empty TopStruct
for Y0 being non empty SubSpace of Y
for A being Subset of Y st A = the carrier of Y0 holds
( A is T_0 iff Y0 is T_0 )

proof end;

theorem :: TSP_1:16

for Y being non empty TopStruct
for Y0 being non empty SubSpace of Y
for Y1 being non empty V91 SubSpace of Y st Y0 is SubSpace of Y1 holds
Y0 is T_0

proof end;

theorem :: TSP_1:17

for X being non empty TopSpace
for X1 being non empty V91 SubSpace of X
for X2 being non empty SubSpace of X st X1 meets X2 holds
X1 meet X2 is T_0

proof end;

theorem :: TSP_1:18

for X being non empty TopSpace
for X1, X2 being non empty V91 SubSpace of X st ( X1 is open or X2 is open ) holds
X1 union X2 is T_0

proof end;

theorem :: TSP_1:19

for X being non empty TopSpace
for X1, X2 being non empty V91 SubSpace of X st ( X1 is closed or X2 is closed ) holds
X1 union X2 is T_0

proof end;

definition

let X be non empty TopSpace;
mode Kolmogorov_subspace of X is non empty V91 SubSpace of X;

end;

theorem :: TSP_1:20

for X being non empty TopSpace
for A0 being non empty Subset of X st A0 is T_0 holds
ex X0 being strict Kolmogorov_subspace of X st A0 = the carrier of X0

proof end;

registration

let X be non empty non trivial TopSpace;
cluster strict proper SubSpace of X;
existence

proof end;

end;

registration

let X be Kolmogorov_space;
cluster non empty -> non empty V91 SubSpace of X;
coherence

proof end;

end;

registration

let X be non-Kolmogorov_space;
cluster non empty non proper -> non empty non trivial V91 SubSpace of X;
coherence

proof end;

cluster non empty V91 -> non empty proper SubSpace of X;
coherence

proof end;

end;

registration

let X be non-Kolmogorov_space;
cluster strict V91 SubSpace of X;
existence

proof end;

end;

definition

let X be non-Kolmogorov_space;
mode non-Kolmogorov_subspace of X is V91 SubSpace of X;

end;

theorem :: TSP_1:21

for X being non empty non-Kolmogorov_space
for A0 being Subset of X st not A0 is T_0 holds
ex X0 being strict non-Kolmogorov_subspace of X st A0 = the carrier of X0

proof end;