:: The {N}agata-Smirnov Theorem. {P}art {I}
:: by Karol P\c{a}k
::
:: Received May 31, 2004
:: Copyright (c) 2004-2021 Association of Mizar Users

Lm1: for r, s, t being Real st r >= 0 & s >= 0 & r + s < t holds
( r < t & s < t )

proof end;

Lm2: for r1, r2, r3, r4 being Real holds |.(r1 - r4).| <= (|.(r1 - r2).| + |.(r2 - r3).|) + |.(r3 - r4).|

proof end;

definition

let T be TopSpace;
let F be Subset-Family of T;

attr F is discrete means :Def1: :: NAGATA_1:def 1
for p being Point of T ex O being open Subset of T st
( p in O & ( for A, B being Subset of T st A in F & B in F & O meets A & O meets B holds
A = B ) );

end;

:: deftheorem Def1 defines discrete NAGATA_1:def 1 :
for T being TopSpace
for F being Subset-Family of T holds
( F is discrete iff for p being Point of T ex O being open Subset of T st
( p in O & ( for A, B being Subset of T st A in F & B in F & O meets A & O meets B holds
A = B ) ) );

registration

let T be non empty TopSpace;

cluster discrete for Element of bool (bool the carrier of T);

existence
ex b₁ being Subset-Family of T st b₁ is discrete

proof end;

end;

registration

let T be non empty TopSpace;

cluster empty discrete for Element of bool (bool the carrier of T);

existence
ex b₁ being Subset-Family of T st
( b₁ is empty & b₁ is discrete )

proof end;

end;

theorem Th1: :: NAGATA_1:1

for T being non empty TopSpace
for F being Subset-Family of T st ex A being Subset of T st F = {A} holds
F is discrete

proof end;

theorem Th2: :: NAGATA_1:2

for T being non empty TopSpace
for F, G being Subset-Family of T st F c= G & G is discrete holds
F is discrete

proof end;

theorem :: NAGATA_1:3

for T being non empty TopSpace
for F, G being Subset-Family of T st F is discrete holds
F /\ G is discrete by Th2, XBOOLE_1:17;

theorem :: NAGATA_1:4

for T being non empty TopSpace
for F, G being Subset-Family of T st F is discrete holds
F \ G is discrete by Th2, XBOOLE_1:36;

theorem :: NAGATA_1:5

for T being non empty TopSpace
for F, G, H being Subset-Family of T st F is discrete & G is discrete & INTERSECTION (F,G) = H holds
H is discrete

proof end;

theorem Th6: :: NAGATA_1:6

for T being non empty TopSpace
for F being Subset-Family of T
for A, B being Subset of T st F is discrete & A in F & B in F & not A = B holds
A misses B

proof end;

theorem Th7: :: NAGATA_1:7

for T being non empty TopSpace
for F being Subset-Family of T st F is discrete holds
for p being Point of T ex O being open Subset of T st
( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial )

proof end;

theorem :: NAGATA_1:8

for T being non empty TopSpace
for F being Subset-Family of T holds
( F is discrete iff ( ( for p being Point of T ex O being open Subset of T st
( p in O & (INTERSECTION ({O},F)) \ {{}} is trivial ) ) & ( for A, B being Subset of T st A in F & B in F & not A = B holds
A misses B ) ) )

proof end;

Lm3: for T being non empty TopSpace
for O being open Subset of T
for A being Subset of T st O meets Cl A holds
O meets A

proof end;

registration

let T be non empty TopSpace;
let F be discrete Subset-Family of T;

cluster clf F -> discrete ;

coherence
clf F is discrete

proof end;

end;

Lm4: for T being non empty TopSpace
for F being Subset-Family of T
for A being Subset of T st A in F holds
Cl A c= Cl (union F)

proof end;

theorem :: NAGATA_1:9

for T being non empty TopSpace
for F being Subset-Family of T st F is discrete holds
for A, B being Subset of T st A in F & B in F holds
Cl (A /\ B) = (Cl A) /\ (Cl B)

proof end;

theorem :: NAGATA_1:10

for T being non empty TopSpace
for F being Subset-Family of T st F is discrete holds
Cl (union F) = union (clf F)

proof end;

theorem Th11: :: NAGATA_1:11

for T being non empty TopSpace
for F being Subset-Family of T st F is discrete holds
F is locally_finite

proof end;

definition

let T be TopSpace;
mode FamilySequence of T is sequence of (bool (bool the carrier of T));

end;

definition

let T be non empty TopSpace;
let Un be FamilySequence of T;
let n be Element of NAT ;
:: original: .
redefine func Un . n -> Subset-Family of T;
coherence
Un . n is Subset-Family of T

proof end;

end;

definition

let T be non empty TopSpace;
let Un be FamilySequence of T;
:: original: Union
redefine func Union Un -> Subset-Family of T;
coherence
Union Un is Subset-Family of T

proof end;

end;

definition

let T be non empty TopSpace;
let Un be FamilySequence of T;

attr Un is sigma_discrete means :Def2: :: NAGATA_1:def 2
for n being Element of NAT holds Un . n is discrete ;

end;

:: deftheorem Def2 defines sigma_discrete NAGATA_1:def 2 :
for T being non empty TopSpace
for Un being FamilySequence of T holds
( Un is sigma_discrete iff for n being Element of NAT holds Un . n is discrete );

Lm5: for T being non empty TopSpace ex Un being FamilySequence of T st Un is sigma_discrete

proof end;

registration

let T be non empty TopSpace;

cluster Relation-like omega -defined bool (bool the carrier of T) -valued Function-like non empty V14( omega ) quasi_total sigma_discrete for Element of bool [:omega,(bool (bool the carrier of T)):];

existence
ex b₁ being FamilySequence of T st b₁ is sigma_discrete by Lm5;

end;

definition

let T be non empty TopSpace;
let Un be FamilySequence of T;

attr Un is sigma_locally_finite means :: NAGATA_1:def 3
for n being Element of NAT holds Un . n is locally_finite ;

end;

:: deftheorem defines sigma_locally_finite NAGATA_1:def 3 :
for T being non empty TopSpace
for Un being FamilySequence of T holds
( Un is sigma_locally_finite iff for n being Element of NAT holds Un . n is locally_finite );

definition

let T be non empty TopSpace;
let F be Subset-Family of T;

attr F is sigma_discrete means :: NAGATA_1:def 4
ex f being sigma_discrete FamilySequence of T st F = Union f;

end;

:: deftheorem defines sigma_discrete NAGATA_1:def 4 :
for T being non empty TopSpace
for F being Subset-Family of T holds
( F is sigma_discrete iff ex f being sigma_discrete FamilySequence of T st F = Union f );

registration

let T be non empty TopSpace;

cluster Relation-like omega -defined bool (bool the carrier of T) -valued Function-like non empty V14( omega ) quasi_total sigma_locally_finite for Element of bool [:omega,(bool (bool the carrier of T)):];

existence
ex b₁ being FamilySequence of T st b₁ is sigma_locally_finite

proof end;

end;

theorem :: NAGATA_1:12

for T being non empty TopSpace
for Un being FamilySequence of T st Un is sigma_discrete holds
Un is sigma_locally_finite by Th11;

theorem :: NAGATA_1:13

for A being uncountable set ex F being Subset-Family of (1TopSp [:A,A:]) st
( F is locally_finite & not F is sigma_discrete )

proof end;

definition

let T be non empty TopSpace;
let Un be FamilySequence of T;

attr Un is Basis_sigma_discrete means :: NAGATA_1:def 5
( Un is sigma_discrete & Union Un is Basis of T );

end;

:: deftheorem defines Basis_sigma_discrete NAGATA_1:def 5 :
for T being non empty TopSpace
for Un being FamilySequence of T holds
( Un is Basis_sigma_discrete iff ( Un is sigma_discrete & Union Un is Basis of T ) );

definition

let T be non empty TopSpace;
let Un be FamilySequence of T;

attr Un is Basis_sigma_locally_finite means :: NAGATA_1:def 6
( Un is sigma_locally_finite & Union Un is Basis of T );

end;

:: deftheorem defines Basis_sigma_locally_finite NAGATA_1:def 6 :
for T being non empty TopSpace
for Un being FamilySequence of T holds
( Un is Basis_sigma_locally_finite iff ( Un is sigma_locally_finite & Union Un is Basis of T ) );

theorem Th14: :: NAGATA_1:14

for r being Real
for PM being non empty MetrSpace
for x being Element of PM holds ([#] PM) \ (cl_Ball (x,r)) in Family_open_set PM

proof end;

theorem :: NAGATA_1:15

for T being non empty TopSpace st T is metrizable holds
( T is regular & T is T_1 )

proof end;

theorem :: NAGATA_1:16

for T being non empty TopSpace st T is metrizable holds
ex Un being FamilySequence of T st Un is Basis_sigma_locally_finite

proof end;

Lm6: for T being non empty TopSpace
for U being open Subset of T
for A being Subset of T st A is closed holds
U \ A is open

proof end;

theorem Th17: :: NAGATA_1:17

for T being non empty TopSpace
for U being sequence of (bool the carrier of T) st ( for n being Element of NAT holds U . n is open ) holds
Union U is open

proof end;

theorem Th18: :: NAGATA_1:18

for T being non empty TopSpace st ( for A being Subset of T
for U being open Subset of T st A is closed & U is open & A c= U holds
ex W being sequence of (bool the carrier of T) st
( A c= Union W & Union W c= U & ( for n being Element of NAT holds
( Cl (W . n) c= U & W . n is open ) ) ) ) holds
T is normal

proof end;

theorem Th19: :: NAGATA_1:19

for T being non empty TopSpace st T is regular holds
for Bn being FamilySequence of T st Union Bn is Basis of T holds
for U being Subset of T
for p being Point of T st U is open & p in U holds
ex O being Subset of T st
( p in O & Cl O c= U & O in Union Bn )

proof end;

theorem :: NAGATA_1:20

for T being non empty TopSpace st T is regular & ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite holds
T is normal

proof end;

Lm7: for r being Real
for A being Point of RealSpace st r > 0 holds
A in Ball (A,r)

proof end;

definition

let T be non empty TopSpace;
let F, G be RealMap of T;

:: original: +
redefine func F + G -> RealMap of T means :Def7: :: NAGATA_1:def 7
for t being Element of T holds it . t = (F . t) + (G . t);

coherence
F + G is RealMap of T

proof end;

compatibility
for b₁ being RealMap of T holds
( b₁ = F + G iff for t being Element of T holds b₁ . t = (F . t) + (G . t) )

proof end;

end;

:: deftheorem Def7 defines + NAGATA_1:def 7 :
for T being non empty TopSpace
for F, G, b₄ being RealMap of T holds
( b₄ = F + G iff for t being Element of T holds b₄ . t = (F . t) + (G . t) );

theorem :: NAGATA_1:21

for T being non empty TopSpace
for f being RealMap of T st f is continuous holds
for F being RealMap of [:T,T:] st ( for x, y being Element of T holds F . (x,y) = |.((f . x) - (f . y)).| ) holds
F is continuous

proof end;

theorem Th22: :: NAGATA_1:22

for T being non empty TopSpace
for F, G being RealMap of T st F is continuous & G is continuous holds
F + G is continuous

proof end;

theorem Th23: :: NAGATA_1:23

for T being non empty TopSpace
for ADD being BinOp of (Funcs ( the carrier of T,REAL)) st ( for f1, f2 being RealMap of T holds ADD . (f1,f2) = f1 + f2 ) holds
( ADD is having_a_unity & ADD is commutative & ADD is associative )

proof end;

theorem Th24: :: NAGATA_1:24

for T being non empty TopSpace
for ADD being BinOp of (Funcs ( the carrier of T,REAL)) st ( for f1, f2 being RealMap of T holds ADD . (f1,f2) = f1 + f2 ) holds
for map9 being Element of Funcs ( the carrier of T,REAL) st map9 is_a_unity_wrt ADD holds
map9 is continuous

proof end;

definition

let A, B be non empty set ;
let F be Function of A,(Funcs (A,B));

func F Toler -> Function of A,B means :Def8: :: NAGATA_1:def 8
for p being Element of A holds it . p = (F . p) . p;

existence
ex b₁ being Function of A,B st
for p being Element of A holds b₁ . p = (F . p) . p

proof end;

uniqueness
for b₁, b₂ being Function of A,B st ( for p being Element of A holds b₁ . p = (F . p) . p ) & ( for p being Element of A holds b₂ . p = (F . p) . p ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines Toler NAGATA_1:def 8 :
for A, B being non empty set
for F being Function of A,(Funcs (A,B))
for b₄ being Function of A,B holds
( b₄ = F Toler iff for p being Element of A holds b₄ . p = (F . p) . p );

theorem :: NAGATA_1:25

for T being non empty TopSpace
for ADD being BinOp of (Funcs ( the carrier of T,REAL)) st ( for f1, f2 being RealMap of T holds ADD . (f1,f2) = f1 + f2 ) holds
for F being FinSequence of Funcs ( the carrier of T,REAL) st ( for n being Element of NAT st 0 <> n & n <= len F holds
F . n is continuous RealMap of T ) holds
ADD "**" F is continuous RealMap of T

proof end;

theorem :: NAGATA_1:26

for T, T1 being non empty TopSpace
for F being Function of the carrier of T,(Funcs ( the carrier of T, the carrier of T1)) st ( for p being Point of T holds F . p is continuous Function of T,T1 ) holds
for S being Function of the carrier of T,(bool the carrier of T) st ( for p being Point of T holds
( p in S . p & S . p is open & ( for p, q being Point of T st p in S . q holds
(F . p) . p = (F . q) . p ) ) ) holds
F Toler is continuous

proof end;

definition

let X be set ;
let r be Real;
let f be Function of X,REAL;
deffunc H₁( Element of X) -> object = min (r,(f . $1));

func min (r,f) -> Function of X,REAL means :Def9: :: NAGATA_1:def 9
for x being set st x in X holds
it . x = min (r,(f . x));

existence
ex b₁ being Function of X,REAL st
for x being set st x in X holds
b₁ . x = min (r,(f . x))

proof end;

uniqueness
for b₁, b₂ being Function of X,REAL st ( for x being set st x in X holds
b₁ . x = min (r,(f . x)) ) & ( for x being set st x in X holds
b₂ . x = min (r,(f . x)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines min NAGATA_1:def 9 :
for X being set
for r being Real
for f, b₄ being Function of X,REAL holds
( b₄ = min (r,f) iff for x being set st x in X holds
b₄ . x = min (r,(f . x)) );

theorem :: NAGATA_1:27

for T being non empty TopSpace
for r being Real
for f being RealMap of T st f is continuous holds
min (r,f) is continuous

proof end;

definition

let X be set ;
let f be Function of [:X,X:],REAL;

pred f is_a_pseudometric_of X means :: NAGATA_1:def 10
( f is Reflexive & f is symmetric & f is triangle );

end;

:: deftheorem defines is_a_pseudometric_of NAGATA_1:def 10 :
for X being set
for f being Function of [:X,X:],REAL holds
( f is_a_pseudometric_of X iff ( f is Reflexive & f is symmetric & f is triangle ) );

Lm8: for X being set
for f being Function of [:X,X:],REAL holds
( f is_a_pseudometric_of X iff for a, b, c being Element of X holds
( f . (a,a) = 0 & f . (a,b) = f . (b,a) & f . (a,c) <= (f . (a,b)) + (f . (b,c)) ) )
by METRIC_1:def 2, METRIC_1:def 4, METRIC_1:def 5;

theorem Th28: :: NAGATA_1:28

for X being set
for f being Function of [:X,X:],REAL holds
( f is_a_pseudometric_of X iff for a, b, c being Element of X holds
( f . (a,a) = 0 & f . (a,c) <= (f . (a,b)) + (f . (c,b)) ) )

proof end;

Lm9: for r being Real
for X being non empty set
for f being Function of [:X,X:],REAL
for x, y being Element of X holds (min (r,f)) . (x,y) = min (r,(f . (x,y)))

proof end;

theorem Th29: :: NAGATA_1:29

for X being set
for f being Function of [:X,X:],REAL st f is_a_pseudometric_of X holds
for x, y being Element of X holds f . (x,y) >= 0

proof end;

theorem Th30: :: NAGATA_1:30

for T being non empty TopSpace
for r being Real
for m being Function of [: the carrier of T, the carrier of T:],REAL st r > 0 & m is_a_pseudometric_of the carrier of T holds
min (r,m) is_a_pseudometric_of the carrier of T

proof end;

theorem :: NAGATA_1:31

for T being non empty TopSpace
for r being Real
for m being Function of [: the carrier of T, the carrier of T:],REAL st r > 0 & m is_metric_of the carrier of T holds
min (r,m) is_metric_of the carrier of T

proof end;