:: The {N}agata-Smirnov Theorem. {P}art {II}
:: by Karol P\c{a}k
::
:: Received July 22, 2004
:: Copyright (c) 2004 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)

proof end;

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 b₁ being Function of [:NAT ,NAT :], NAT st
for n, m being Element of NAT holds b₁ . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1

proof end;

uniqueness
for b₁, b₂ being Function of [:NAT ,NAT :], NAT st ( for n, m being Element of NAT holds b₁ . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1 ) & ( for n, m being Element of NAT holds b₂ . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines PairFunc NAGATA_2:def 1 :

for b₁ being Function of [:NAT ,NAT :], NAT holds
( b₁ = PairFunc iff for n, m being Element of NAT holds b₁ . [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 b₁ being Function of X, REAL st
for y being Element of X holds b₁ . y = f . x,y

proof end;

uniqueness
for b₁, b₂ being Function of X, REAL st ( for y being Element of X holds b₁ . y = f . x,y ) & ( for y being Element of X holds b₂ . y = f . x,y ) holds
b₁ = b₂

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 b₄ being Function of X, REAL holds
( b₄ = dist f,x iff for y being Element of X holds b₄ . y = f . x,y );

theorem Th3: :: NAGATA_2:3

for T1, T2 being non empty TopSpace
for D being Subset of st D is open holds
for x1 being Point of
for x2 being Point of
for X1 being Subset of
for X2 being Subset of 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 pmet' being RealMap of [:T,T:] st pmet = pmet' holds
pmet' is continuous ) holds
for x being Point of 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 ;
func inf f,A -> Function of X, REAL means :Def3: :: NAGATA_2:def 3
for x being Element of X holds it . x = inf ((dist f,x) .: A);
existence
ex b₁ being Function of X, REAL st
for x being Element of X holds b₁ . x = inf ((dist f,x) .: A)

proof end;

uniqueness
for b₁, b₂ being Function of X, REAL st ( for x being Element of X holds b₁ . x = inf ((dist f,x) .: A) ) & ( for x being Element of X holds b₂ . x = inf ((dist f,x) .: A) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines inf NAGATA_2:def 3 :

for X being non empty set
for f being Function of [:X,X:], REAL
for A being Subset of
for b₄ being Function of X, REAL holds
( b₄ = inf f,A iff for x being Element of X holds b₄ . x = inf ((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
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
for x being Element of X holds (inf 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
for x being Element of X st x in A holds
(inf 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
for A being non empty Subset of holds abs (((inf pmet,A) . x) - ((inf 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 holds dist pmet,p is continuous ) holds
for A being non empty Subset of holds inf 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 holds Cl A = { p where p is Point of : (inf 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 Element of 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 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)

proof end;

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

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 Element of NAT ex f being RealMap of T st
( FS1 . n = f & f is continuous & ( for p being Point of holds f . p >= 0 ) ) ) & ex seq being Real_Sequence st
( seq is summable & ( for n being Element of NAT
for p being Point of holds (FS1 # p) . n <= seq . n ) ) holds
for f being RealMap of T st ( for p being Point of 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 Element of 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 pmet' being RealMap of [:T,T:] st pmet = pmet' holds
pmet' 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 pmet' being RealMap of [:T,T:] st pmet = pmet' holds
pmet' 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 pmet' being RealMap of [:T,T:] st pmet = pmet' holds
pmet' is continuous ) holds
for A being non empty Subset of
for p being Point of st p in Cl A holds
(inf 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 Element of 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 pmet' being RealMap of [:T,T:] st pmet = pmet' holds
pmet' is continuous ) ) ) & ( for p being Point of
for A' being non empty Subset of st not p in A' & A' 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
(inf pmet,A') . 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;

registration

let T1, T2 be TopSpace;
let f be RealMap of [:T1,T2:];
let t1 be Point of ;
let t2 be Point of ;
cluster f . t1,t2 -> real ;
coherence
f . t1,t2 is real ;

end;

NAT = rng PairFunc
by Th2, FUNCT_2:def 3;

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

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

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;