:: On Kolmogorov Topological Spaces
:: by Zbigniew Karno
::
:: Received July 26, 1994
:: 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 b₁ being TopStruct holds
( b₁ is SubSpace of Y iff ( the carrier of b₁ c= the carrier of Y & ( for G0 being Subset of b₁ holds
( G0 is open iff ex G being Subset of Y st
( G is open & G0 = G /\ the carrier of b₁ ) ) ) ) )

proof end;

end;

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

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 b₁ being TopStruct holds
( b₁ is SubSpace of Y iff ( the carrier of b₁ c= the carrier of Y & ( for F0 being Subset of b₁ holds
( F0 is closed iff ex F being Subset of Y st
( F is closed & F0 = F /\ the carrier of b₁ ) ) ) ) )

proof end;

end;

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

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 b₁ being non empty TopStruct st b₁ is trivial holds
b₁ is T_0

proof end;

end;

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

proof end;

registration

cluster non empty strict TopSpace-like T_0 for TopStruct ;

existence
ex b₁ being TopSpace st
( b₁ is strict & b₁ is T_0 & not b₁ is empty )

proof end;

cluster non empty strict TopSpace-like non T_0 for TopStruct ;

existence
ex b₁ being TopSpace st
( b₁ is strict & not b₁ is T_0 & not b₁ is empty )

proof end;

end;

registration

cluster non empty TopSpace-like discrete -> non empty T_0 for TopStruct ;

coherence
for b₁ being non empty TopSpace st b₁ is discrete holds
b₁ is T_0

proof end;

cluster non empty TopSpace-like non T_0 -> non empty non discrete for TopStruct ;

coherence
for b₁ being non empty TopSpace st not b₁ is T_0 holds
not b₁ is discrete ;

cluster non empty non trivial TopSpace-like anti-discrete -> non empty non T_0 for TopStruct ;

coherence
for b₁ being non empty TopSpace st b₁ is anti-discrete & not b₁ is trivial holds
not b₁ is T_0 by Lm1;

cluster non empty TopSpace-like T_0 anti-discrete -> non empty trivial for TopStruct ;

coherence
for b₁ being non empty TopSpace st b₁ is anti-discrete & b₁ is T_0 holds
b₁ is trivial ;

cluster non empty non trivial TopSpace-like T_0 -> non empty non anti-discrete for TopStruct ;

coherence
for b₁ being non empty TopSpace st b₁ is T_0 & not b₁ is trivial holds
not b₁ 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

cluster non empty TopSpace-like T_0 almost_discrete -> non empty discrete for TopStruct ;

coherence
for b₁ being non empty TopSpace st b₁ is almost_discrete & b₁ is T_0 holds
b₁ is discrete

proof end;

cluster non empty TopSpace-like non discrete almost_discrete -> non empty non T_0 for TopStruct ;

coherence
for b₁ being non empty TopSpace st b₁ is almost_discrete & not b₁ is discrete holds
not b₁ is T_0 ;

cluster non empty TopSpace-like T_0 non discrete -> non empty non almost_discrete for TopStruct ;

coherence
for b₁ being non empty TopSpace st not b₁ is discrete & b₁ is T_0 holds
not b₁ is almost_discrete ;

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 empty non trivial strict TopSpace-like T_0 for TopStruct ;

existence
ex b₁ being Kolmogorov_space st
( not b₁ is trivial & b₁ is strict )

proof end;

cluster non empty non trivial strict TopSpace-like non T_0 non discrete for TopStruct ;

existence
ex b₁ being non-Kolmogorov_space st
( not b₁ is trivial & b₁ 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 Th9, TEX_2:30;

:: 4. Kolmogorov Subspaces.

registration

let Y be non empty TopStruct ;

cluster non empty strict T_0 for SubSpace of Y;

existence
ex b₁ being SubSpace of Y st
( b₁ is strict & b₁ is T_0 & not b₁ 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 b₁ being Kolmogorov_subspace of X st
( b₁ is proper & b₁ is strict )

proof end;

end;

registration

let X be Kolmogorov_space;

cluster non empty -> non empty V144() for SubSpace of X;

coherence
for b₁ being non empty SubSpace of X holds b₁ 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 b₁ being non empty SubSpace of X st not b₁ is proper holds
not b₁ is V144()

proof end;

cluster non empty V144() -> non empty proper for SubSpace of X;

coherence
for b₁ being non empty SubSpace of X st b₁ is V144() holds
b₁ is proper ;

end;

registration

let X be non-Kolmogorov_space;

cluster strict V144() for SubSpace of X;

existence
ex b₁ being SubSpace of X st
( b₁ is strict & b₁ is V144() )

proof end;

end;

definition

let X be non-Kolmogorov_space;
mode non-Kolmogorov_subspace of X is V144() SubSpace of X;

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;