:: The {N}agata-Smirnov Theorem. {P}art {II}
:: by Karol P\c{a}k
::
:: Received July 22, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

theorem Th1: :: NAGATA_2:1
for i being Element of NAT st i > 0 holds
ex n, m being Element of NAT st i = (2 |^ n) * ((2 * m) + 1)
proofend;

definition
func PairFunc  ->  Function of [:NAT,NAT:],NAT means :Def1: :: NAGATA_2:def 1
 for n, m being Element of NAT holds it . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1;
existence
 ex b1 being Function of [:NAT,NAT:],NAT st
for n, m being Element of NAT holds b1 . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1
proofend;
uniqueness
 for b1, b2 being Function of [:NAT,NAT:],NAT st ( for n, m being Element of NAT holds b1 . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1 ) & ( for n, m being Element of NAT holds b2 . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1 ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines PairFunc NAGATA_2:def_1_:_
 for b1 being Function of [:NAT,NAT:],NAT holds
( b1 = PairFunc iff for n, m being Element of NAT holds b1 . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1 );

theorem Th2: :: NAGATA_2:2
PairFunc is bijective
proofend;

definition
let X be set ;
let f be Function of [:X,X:],REAL;
let x be Element of X;
func dist (f,x) ->  Function of X,REAL means :Def2: :: NAGATA_2:def 2
 for y being Element of X holds it . y = f . (x,y);
existence
 ex b1 being Function of X,REAL st
for y being Element of X holds b1 . y = f . (x,y)
proofend;
uniqueness
 for b1, b2 being Function of X,REAL st ( for y being Element of X holds b1 . y = f . (x,y) ) & ( for y being Element of X holds b2 . y = f . (x,y) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines dist NAGATA_2:def_2_:_
 for X being set
for f being Function of [:X,X:],REAL
for x being Element of X
for b4 being Function of X,REAL holds
( b4 = dist (f,x) iff for y being Element of X holds b4 . y = f . (x,y) );

theorem Th3: :: NAGATA_2:3
for T1, T2 being non empty TopSpace
for D being Subset of [:T1,T2:] st D is open holds
for x1 being Point of T1
for x2 being Point of T2
for X1 being Subset of T1
for X2 being Subset of T2 holds
( ( X1 = (pr1 ( the carrier of T1, the carrier of T2)) .: (D /\ [: the carrier of T1,{x2}:]) implies X1 is open ) & ( X2 = (pr2 ( the carrier of T1, the carrier of T2)) .: (D /\ [:{x1}, the carrier of T2:]) implies X2 is open ) )
proofend;

theorem Th4: :: NAGATA_2:4
for T being non empty TopSpace
for pmet being Function of [: the carrier of T, the carrier of T:],REAL st ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) holds
for x being Point of T holds dist (pmet,x) is continuous
proofend;

definition
let X be non empty set ;
let f be Function of [:X,X:],REAL;
let A be Subset of X;
func lower_bound (f,A) ->  Function of X,REAL means :Def3: :: NAGATA_2:def 3
 for x being Element of X holds it . x = lower_bound ((dist (f,x)) .: A);
existence
 ex b1 being Function of X,REAL st
for x being Element of X holds b1 . x = lower_bound ((dist (f,x)) .: A)
proofend;
uniqueness
 for b1, b2 being Function of X,REAL st ( for x being Element of X holds b1 . x = lower_bound ((dist (f,x)) .: A) ) & ( for x being Element of X holds b2 . x = lower_bound ((dist (f,x)) .: A) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines lower_bound NAGATA_2:def_3_:_
 for X being non empty set
for f being Function of [:X,X:],REAL
for A being Subset of X
for b4 being Function of X,REAL holds
( b4 = lower_bound (f,A) iff for x being Element of X holds b4 . x = lower_bound ((dist (f,x)) .: A) );

Lm1:  for X being non empty set
for f being Function of [:X,X:],REAL st f is_a_pseudometric_of X holds
( f is bounded_below & ( for A being non empty Subset of X
for x being Element of X holds
( not (dist (f,x)) .: A is empty & (dist (f,x)) .: A is bounded_below ) ) )
proofend;

theorem Th5: :: NAGATA_2:5
for X being non empty set
for f being Function of [:X,X:],REAL st f is_a_pseudometric_of X holds
for A being non empty Subset of X
for x being Element of X holds (lower_bound (f,A)) . x >= 0
proofend;

theorem Th6: :: NAGATA_2:6
for X being non empty set
for f being Function of [:X,X:],REAL st f is_a_pseudometric_of X holds
for A being Subset of X
for x being Element of X st x in A holds
(lower_bound (f,A)) . x = 0
proofend;

theorem Th7: :: NAGATA_2:7
for T being non empty TopSpace
for pmet being Function of [: the carrier of T, the carrier of T:],REAL st pmet is_a_pseudometric_of the carrier of T holds
for x, y being Point of T
for A being non empty Subset of T holds abs (((lower_bound (pmet,A)) . x) - ((lower_bound (pmet,A)) . y)) <= pmet . (x,y)
proofend;

theorem Th8: :: NAGATA_2:8
for T being non empty TopSpace
for pmet being Function of [: the carrier of T, the carrier of T:],REAL st pmet is_a_pseudometric_of the carrier of T &amp; ( for p being Point of T holds dist (pmet,p) is continuous ) holds
for A being non empty Subset of T holds lower_bound (pmet,A) is continuous
proofend;

theorem Th9: :: NAGATA_2:9
for X being set
for f being Function of [:X,X:],REAL st f is_metric_of X holds
f is_a_pseudometric_of X
proofend;

theorem Th10: :: NAGATA_2:10
for T being non empty TopSpace
for pmet being Function of [: the carrier of T, the carrier of T:],REAL st pmet is_metric_of the carrier of T &amp; ( for A being non empty Subset of T holds Cl A =  {  p where p is Point of T : (lower_bound (pmet,A)) . p = 0  }  ) holds
T is metrizable
proofend;

theorem Th11: :: NAGATA_2:11
for T being non empty TopSpace
for FS2 being Functional_Sequence of [: the carrier of T, the carrier of T:],REAL st ( for n being Element of NAT ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( FS2 . n = pmet &amp; pmet is_a_pseudometric_of the carrier of T ) ) &amp; ( for pq being Element of [: the carrier of T, the carrier of T:] holds FS2 # pq is summable ) holds
for pmet being Function of [: the carrier of T, the carrier of T:],REAL st ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (FS2 # pq) ) holds
pmet is_a_pseudometric_of the carrier of T
proofend;

theorem Th12: :: NAGATA_2:12
for r being Real
for n being Element of NAT
for seq being Real_Sequence st ( for m being Element of NAT st m <= n holds
seq . m <= r ) holds
for m being Element of NAT st m <= n holds
(Partial_Sums seq) . m <= r * (m + 1)
proofend;

theorem Th13: :: NAGATA_2:13
for seq being Real_Sequence
for k being Element of NAT holds abs ((Partial_Sums seq) . k) <= (Partial_Sums (abs seq)) . k
proofend;

theorem Th14: :: NAGATA_2:14
for T being non empty TopSpace
for FS1 being Functional_Sequence of the carrier of T,REAL st ( for n being Element of NAT ex f being RealMap of T st
( FS1 . n = f &amp; f is continuous &amp; ( for p being Point of T holds f . p >= 0 ) ) ) &amp; ex seq being Real_Sequence st
( seq is summable &amp; ( for n being Element of NAT
for p being Point of T holds (FS1 # p) . n <= seq . n ) ) holds
for f being RealMap of T st ( for p being Point of T holds f . p = Sum (FS1 # p) ) holds
f is continuous
proofend;

theorem Th15: :: NAGATA_2:15
for T being non empty TopSpace
for s being Real
for FS2 being Functional_Sequence of [: the carrier of T, the carrier of T:],REAL st ( for n being Element of NAT ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( FS2 . n = pmet &amp; pmet is_a_pseudometric_of the carrier of T &amp; ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq <= s ) &amp; ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) ) ) holds
for pmet being Function of [: the carrier of T, the carrier of T:],REAL st ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (((1 / 2) GeoSeq) (#) (FS2 # pq)) ) holds
( pmet is_a_pseudometric_of the carrier of T &amp; ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) )
proofend;

theorem Th16: :: NAGATA_2:16
for T being non empty TopSpace
for pmet being Function of [: the carrier of T, the carrier of T:],REAL st pmet is_a_pseudometric_of the carrier of T &amp; ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) holds
for A being non empty Subset of T
for p being Point of T st p in Cl A holds
(lower_bound (pmet,A)) . p = 0
proofend;

theorem Th17: :: NAGATA_2:17
for T being non empty TopSpace st T is T_1 holds
for s being Real
for FS2 being Functional_Sequence of [: the carrier of T, the carrier of T:],REAL st ( for n being Element of NAT ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( FS2 . n = pmet &amp; pmet is_a_pseudometric_of the carrier of T &amp; ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq <= s ) &amp; ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) ) ) &amp; ( for p being Point of T
for A9 being non empty Subset of T st not p in A9 &amp; A9 is closed holds
ex n being Element of NAT st
for pmet being Function of [: the carrier of T, the carrier of T:],REAL st FS2 . n = pmet holds
(lower_bound (pmet,A9)) . p > 0 ) holds
( ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( pmet is_metric_of the carrier of T &amp; ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (((1 / 2) GeoSeq) (#) (FS2 # pq)) ) ) &amp; T is metrizable )
proofend;

theorem Th18: :: NAGATA_2:18
for D being non empty set
for p, q being FinSequence of D
for B being BinOp of D st p is one-to-one &amp; q is one-to-one &amp; rng q c= rng p &amp; B is commutative &amp; B is associative &amp; ( B is having_a_unity or ( len q >= 1 &amp; len p > len q ) ) holds
ex r being FinSequence of D st
( r is one-to-one &amp; rng r = (rng p) \ (rng q) &amp; B "**" p = B . ((B "**" q),(B "**" r)) )
proofend;

registration
let T1, T2 be TopSpace;
let f be RealMap of [:T1,T2:];
let t1 be Point of T1;
let t2 be Point of T2;
clusterf . (t1,t2) ->  real ;
coherence
 f . (t1,t2) is real ;
end;

Lm2:  PairFunc " = PairFunc "
by Th2, TOPS_2:def_4;

:: [WP: ] Nagata-Smirnov_Theorem
theorem Th19: :: NAGATA_2:19
for T being non empty TopSpace holds
( ( T is regular &amp; T is T_1 &amp; ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite ) iff T is metrizable )
proofend;

theorem Th20: :: NAGATA_2:20
for T being non empty TopSpace st T is metrizable holds
for FX being Subset-Family of T st FX is Cover of T &amp; FX is open holds
ex Un being FamilySequence of T st
( Union Un is open &amp; Union Un is Cover of T &amp; Union Un is_finer_than FX &amp; Un is sigma_discrete )
proofend;

theorem Th21: :: NAGATA_2:21
for T being non empty TopSpace st T is metrizable holds
ex Un being FamilySequence of T st Un is Basis_sigma_discrete
proofend;

:: [WP: ] Bing_Theorem
theorem :: NAGATA_2:22
for T being non empty TopSpace holds
( ( T is regular &amp; T is T_1 &amp; ex Bn being FamilySequence of T st Bn is Basis_sigma_discrete ) iff T is metrizable )
proofend;