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


theorem Th1: :: NAGATA_2:1
for i being Nat st i > 0 holds
ex n, m being Nat st i = (2 |^ n) * ((2 * m) + 1)
proof end;

definition
func PairFunc -> Function of [:NAT,NAT:],NAT means :Def1: :: NAGATA_2:def 1
 for n, m being 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 Nat holds b1 . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1
proof end;
uniqueness
for b1, b2 being Function of [:NAT,NAT:],NAT st ( for n, m being Nat holds b1 . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1 ) & ( for n, m being Nat holds b2 . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1 ) holds
b1 = b2
proof end;
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 Nat holds b1 . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1 );

theorem Th2: :: NAGATA_2:2
PairFunc is bijective
proof end;

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)
proof end;
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
proof end;
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 ) )
proof end;

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
proof end;

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)
proof end;
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
proof end;
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 ) ) )
proof end;

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
proof end;

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
proof end;

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 |.(((lower_bound (pmet,A)) . x) - ((lower_bound (pmet,A)) . y)).| <= pmet . (x,y)
proof end;

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 & ( 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
proof end;

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
proof end;

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 & ( 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
proof end;

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 Nat ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( FS2 . n = pmet & pmet is_a_pseudometric_of the carrier of T ) ) & ( 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
proof end;

theorem Th12: :: NAGATA_2:12
for r being Real
for n being Nat
for seq being Real_Sequence st ( for m being Nat st m <= n holds
seq . m <= r ) holds
for m being Nat st m <= n holds
(Partial_Sums seq) . m <= r * (m + 1)
proof end;

theorem Th13: :: NAGATA_2:13
for seq being Real_Sequence
for k being Nat holds |.((Partial_Sums seq) . k).| <= (Partial_Sums (abs seq)) . k
proof end;

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 Nat ex f being RealMap of T st
( FS1 . n = f & f is continuous & ( for p being Point of T holds f . p >= 0 ) ) ) & ex seq being Real_Sequence st
( seq is summable & ( for n being 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
proof end;

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 Nat ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( FS2 . n = pmet & pmet is_a_pseudometric_of the carrier of T & ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq <= s ) & ( 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 & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) )
proof end;

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 & ( 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
proof end;

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 Nat ex pmet being Function of [: the carrier of T, the carrier of T:],REAL st
( FS2 . n = pmet & pmet is_a_pseudometric_of the carrier of T & ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq <= s ) & ( for pmet9 being RealMap of [:T,T:] st pmet = pmet9 holds
pmet9 is continuous ) ) ) & ( for p being Point of T
for A9 being non empty Subset of T st not p in A9 & A9 is closed holds
ex n being 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 & ( for pq being Element of [: the carrier of T, the carrier of T:] holds pmet . pq = Sum (((1 / 2) GeoSeq) (#) (FS2 # pq)) ) ) & T is metrizable )
proof end;

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 & q is one-to-one & rng q c= rng p & B is commutative & B is associative & ( B is having_a_unity or ( len q >= 1 & len p > len q ) ) holds
ex r being FinSequence of D st
( r is one-to-one & rng r = (rng p) \ (rng q) & B "**" p = B . ((B "**" q),(B "**" r)) )
proof end;

Lm2: PairFunc " = PairFunc "
by Th2, TOPS_2:def 4;

reconsider jj = 1 as Real ;

:: WP: Nagata-Smirnov metrization theorem
theorem Th19: :: NAGATA_2:19
for T being non empty TopSpace holds
( ( T is regular & T is T_1 & ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite ) iff T is metrizable )
proof end;

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 & FX is open holds
ex Un being FamilySequence of T st
( Union Un is open & Union Un is Cover of T & Union Un is_finer_than FX & Un is sigma_discrete )
proof end;

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
proof end;

:: WP: Bing metrization theorem
theorem :: NAGATA_2:22
for T being non empty TopSpace holds
( ( T is regular & T is T_1 & ex Bn being FamilySequence of T st Bn is Basis_sigma_discrete ) iff T is metrizable )
proof end;