:: 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 b1 being Subset-Family of T st b1 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 b1 being Subset-Family of T st
( b1 is empty & b1 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 b1 being FamilySequence of T st b1 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 b1 being FamilySequence of T st b1 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 b1 being RealMap of T holds
( b1 = F + G iff for t being Element of T holds b1 . t = (F . t) + (G . t) )
proof end;
end;

:: deftheorem Def7 defines + NAGATA_1:def 7 :
for T being non empty TopSpace
for F, G, b4 being RealMap of T holds
( b4 = F + G iff for t being Element of T holds b4 . 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 b1 being Function of A,B st
for p being Element of A holds b1 . p = (F . p) . p
proof end;
uniqueness
for b1, b2 being Function of A,B st ( for p being Element of A holds b1 . p = (F . p) . p ) & ( for p being Element of A holds b2 . p = (F . p) . p ) holds
b1 = b2
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 b4 being Function of A,B holds
( b4 = F Toler iff for p being Element of A holds b4 . 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 H1( 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 b1 being Function of X,REAL st
for x being set st x in X holds
b1 . x = min (r,(f . x))
proof end;
uniqueness
for b1, b2 being Function of X,REAL st ( for x being set st x in X holds
b1 . x = min (r,(f . x)) ) & ( for x being set st x in X holds
b2 . x = min (r,(f . x)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines min NAGATA_1:def 9 :
for X being set
for r being Real
for f, b4 being Function of X,REAL holds
( b4 = min (r,f) iff for x being set st x in X holds
b4 . 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;