:: On Kolmogorov Topological Spaces
:: by Zbigniew Karno
::
:: Copyright (c) 1994-2021 Association of Mizar Users

:: 1. Subspaces.
definition
let Y be TopStruct ;
redefine mode SubSpace of Y 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
for b1 being TopStruct holds
( b1 is SubSpace of Y iff ( the carrier of b1 c= the carrier of Y & ( for G0 being Subset of b1 holds
( G0 is open iff ex G being Subset of Y st
( G is open & G0 = G /\ the carrier of b1 ) ) ) ) )
proof end;
end;

:: deftheorem Def1 defines SubSpace TSP_1:def 1 :
for Y, b2 being TopStruct holds
( b2 is SubSpace of Y iff ( the carrier of b2 c= the carrier of Y & ( for G0 being Subset of b2 holds
( G0 is open iff ex G being Subset of Y st
( G is open & G0 = G /\ the carrier of b2 ) ) ) ) );

theorem Th1: :: TSP_1:1
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 ;
redefine mode SubSpace of Y 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
for b1 being TopStruct holds
( b1 is SubSpace of Y iff ( the carrier of b1 c= the carrier of Y & ( for F0 being Subset of b1 holds
( F0 is closed iff ex F being Subset of Y st
( F is closed & F0 = F /\ the carrier of b1 ) ) ) ) )
proof end;
end;

:: deftheorem Def2 defines SubSpace TSP_1:def 2 :
for Y, b2 being TopStruct holds
( b2 is SubSpace of Y iff ( the carrier of b2 c= the carrier of Y & ( for F0 being Subset of b2 holds
( F0 is closed iff ex F being Subset of Y st
( F is closed & F0 = F /\ the carrier of b2 ) ) ) ) );

theorem Th2: :: TSP_1:2
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;

:: 2. Kolmogorov Spaces.
definition
let T be TopStruct ;
redefine attr T is T_0 means :: 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
( T is T_0 iff ( 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 ) ) ) )
proof end;
end;

:: deftheorem defines T_0 TSP_1:def 3 :
for T being TopStruct holds
( T is T_0 iff ( 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 ) ) ) );

definition
let Y be TopStruct ;
redefine attr Y is T_0 means :: 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
( Y is T_0 iff ( 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 ) ) ) )
proof end;
end;

:: deftheorem defines T_0 TSP_1:def 4 :
for Y being TopStruct holds
( Y is T_0 iff ( 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 ) ) ) );

registration
cluster non empty trivial -> non empty T_0 for TopStruct ;
coherence
for b1 being non empty TopStruct st b1 is trivial holds
b1 is T_0
proof end;
end;

Lm1: for X being non trivial anti-discrete TopStruct holds not X is T_0
proof end;

registration
existence
ex b1 being TopSpace st
( b1 is strict & b1 is T_0 & not b1 is empty )
proof end;
existence
ex b1 being TopSpace st
( b1 is strict & not b1 is T_0 & not b1 is empty )
proof end;
end;

registration
coherence
for b1 being non empty TopSpace st b1 is discrete holds
b1 is T_0
proof end;
cluster non empty TopSpace-like non T_0 -> non empty non discrete for TopStruct ;
coherence
for b1 being non empty TopSpace st not b1 is T_0 holds
not b1 is discrete
;
cluster non empty non trivial TopSpace-like anti-discrete -> non empty non T_0 for TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is anti-discrete & not b1 is trivial holds
not b1 is T_0
by Lm1;
coherence
for b1 being non empty TopSpace st b1 is anti-discrete & b1 is T_0 holds
b1 is trivial
;
cluster non empty non trivial TopSpace-like T_0 -> non empty non anti-discrete for TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is T_0 & not b1 is trivial holds
not b1 is anti-discrete
;
end;

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

proof end;

definition
let X be non empty TopSpace;
redefine attr X is T_0 means :: TSP_1:def 5
for x, y being Point of X st x <> y holds
Cl {x} <> Cl {y};
compatibility
( X is T_0 iff for x, y being Point of X st x <> y holds
Cl {x} <> Cl {y} )
proof end;
end;

:: deftheorem defines T_0 TSP_1:def 5 :
for X being non empty TopSpace holds
( X is T_0 iff for x, y being Point of X st x <> y holds
Cl {x} <> Cl {y} );

definition
let X be non empty TopSpace;
redefine attr X is T_0 means :: 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
( X is T_0 iff for x, y being Point of X holds
( not x <> y or not x in Cl {y} or not y in Cl {x} ) )
proof end;
end;

:: deftheorem defines T_0 TSP_1:def 6 :
for X being non empty TopSpace holds
( X is T_0 iff for x, y being Point of X holds
( not x <> y or not x in Cl {y} or not y in Cl {x} ) );

definition
let X be non empty TopSpace;
redefine attr X is T_0 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
( X is T_0 iff for x, y being Point of X st x <> y & x in Cl {y} holds
not Cl {y} c= Cl {x} )
proof end;
end;

:: deftheorem defines T_0 TSP_1:def 7 :
for X being non empty TopSpace holds
( X is T_0 iff for x, y being Point of X st x <> y & x in Cl {y} holds
not Cl {y} c= Cl {x} );

registration
coherence
for b1 being non empty TopSpace st b1 is almost_discrete & b1 is T_0 holds
b1 is discrete
proof end;
cluster non empty TopSpace-like non discrete almost_discrete -> non empty non T_0 for TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is almost_discrete & not b1 is discrete holds
not b1 is T_0
;
cluster non empty TopSpace-like T_0 non discrete -> non empty non almost_discrete for TopStruct ;
coherence
for b1 being non empty TopSpace st not b1 is discrete & b1 is T_0 holds
not b1 is almost_discrete
;
end;

definition end;

registration
existence
ex b1 being Kolmogorov_space st
( not b1 is trivial & b1 is strict )
proof end;
cluster non empty non trivial strict TopSpace-like non T_0 non discrete for TopStruct ;
existence
ex b1 being non-Kolmogorov_space st
( not b1 is trivial & b1 is strict )
proof end;
end;

:: 3. T_{0} Subsets.
definition
let Y be TopStruct ;
let IT be Subset of Y;
attr IT is T_0 means :: 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 defines T_0 TSP_1:def 8 :
for Y being TopStruct
for IT being Subset of Y holds
( IT is T_0 iff 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 ) );

definition
let Y be non empty TopStruct ;
let A be Subset of Y;
redefine attr A is T_0 means :: 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
( A is T_0 iff 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 ) )
proof end;
end;

:: deftheorem defines T_0 TSP_1:def 9 :
for Y being non empty TopStruct
for A being Subset of Y holds
( A is T_0 iff 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 ) );

theorem :: TSP_1:3
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 Th4: :: TSP_1:4
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 ) ;

theorem Th5: :: TSP_1:5
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 ;

theorem Th6: :: TSP_1:6
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 Th7: :: TSP_1:7
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 Th8: :: TSP_1:8
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 Th9: :: TSP_1:9
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:10
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 :: 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
( A is T_0 iff for x, y being Point of X st x in A & y in A & x <> y holds
Cl {x} <> Cl {y} )
proof end;
end;

:: deftheorem defines T_0 TSP_1:def 10 :
for X being non empty TopSpace
for A being Subset of X holds
( A is T_0 iff for x, y being Point of X st x in A & y in A & x <> y holds
Cl {x} <> Cl {y} );

definition
let X be non empty TopSpace;
let A be Subset of X;
redefine attr A is T_0 means :: 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
( A is T_0 iff 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} )
proof end;
end;

:: deftheorem defines T_0 TSP_1:def 11 :
for X being non empty TopSpace
for A being Subset of X holds
( A is T_0 iff 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} );

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
( A is T_0 iff 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} )
proof end;
end;

:: deftheorem defines T_0 TSP_1:def 12 :
for X being non empty TopSpace
for A being Subset of X holds
( A is T_0 iff 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} );

theorem :: TSP_1:11
for X being non empty TopSpace
for A being empty Subset of X holds A is T_0 ;

theorem :: TSP_1:12
for X being non empty TopSpace
for x being Point of X holds {x} is T_0 by ;

:: 4. Kolmogorov Subspaces.
registration
let Y be non empty TopStruct ;
cluster non empty strict T_0 for SubSpace of Y;
existence
ex b1 being SubSpace of Y st
( b1 is strict & b1 is T_0 & not b1 is empty )
proof end;
end;

Lm3: now :: thesis: for Z being TopStruct
for Z0 being SubSpace of Z holds the carrier of Z0 is Subset of Z
let Z be 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 4;
hence the carrier of Z0 is Subset of Z ; :: thesis: verum
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
( Y0 is T_0 iff ( 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 ) ) )
proof end;
end;

:: deftheorem defines T_0 TSP_1:def 13 :
for Y being TopStruct
for Y0 being SubSpace of Y holds
( Y0 is T_0 iff ( 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 ) ) );

definition
let Y be TopStruct ;
let Y0 be SubSpace of Y;
:: original: T_0
redefine attr Y0 is T_0 means :: 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
( Y0 is T_0 iff ( 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 ) ) )
proof end;
end;

:: deftheorem defines T_0 TSP_1:def 14 :
for Y being TopStruct
for Y0 being SubSpace of Y holds
( Y0 is T_0 iff ( 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 ) ) );

theorem Th13: :: TSP_1:13
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 V144() ) ;

theorem :: TSP_1:14
for Y being non empty TopStruct
for Y0 being non empty SubSpace of Y
for Y1 being non empty V144() SubSpace of Y st Y0 is SubSpace of Y1 holds
Y0 is V144()
proof end;

theorem :: TSP_1:15
for X being non empty TopSpace
for X1 being non empty V144() SubSpace of X
for X2 being non empty SubSpace of X st X1 meets X2 holds
X1 meet X2 is V144()
proof end;

theorem :: TSP_1:16
for X being non empty TopSpace
for X1, X2 being non empty V144() SubSpace of X st ( X1 is open or X2 is open ) holds
X1 union X2 is V144()
proof end;

theorem :: TSP_1:17
for X being non empty TopSpace
for X1, X2 being non empty V144() SubSpace of X st ( X1 is closed or X2 is closed ) holds
X1 union X2 is V144()
proof end;

definition
let X be non empty TopSpace;
mode Kolmogorov_subspace of X is non empty V144() SubSpace of X;
end;

theorem :: TSP_1:18
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 trivial TopSpace;
cluster non empty strict T_0 proper for SubSpace of X;
existence
ex b1 being Kolmogorov_subspace of X st
( b1 is proper & b1 is strict )
proof end;
end;

registration
let X be Kolmogorov_space;
cluster non empty -> non empty V144() for SubSpace of X;
coherence
for b1 being non empty SubSpace of X holds b1 is V144()
proof end;
end;

registration
let X be non-Kolmogorov_space;
cluster non empty non proper -> non empty V144() for SubSpace of X;
coherence
for b1 being non empty SubSpace of X st not b1 is proper holds
not b1 is V144()
proof end;
cluster non empty V144() -> non empty proper for SubSpace of X;
coherence
for b1 being non empty SubSpace of X st b1 is V144() holds
b1 is proper
;
end;

registration
let X be non-Kolmogorov_space;
cluster strict V144() for SubSpace of X;
existence
ex b1 being SubSpace of X st
( b1 is strict & b1 is V144() )
proof end;
end;

definition end;

theorem :: TSP_1:19
for X being 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;