:: by Karol P\c{a}k

::

:: Received July 22, 2004

:: Copyright (c) 2004-2021 Association of Mizar Users

definition

ex b_{1} being Function of [:NAT,NAT:],NAT st

for n, m being Nat holds b_{1} . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1

for b_{1}, b_{2} being Function of [:NAT,NAT:],NAT st ( for n, m being Nat holds b_{1} . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1 ) & ( for n, m being Nat holds b_{2} . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1 ) holds

b_{1} = b_{2}
end;

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 for n, m being Nat holds it . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1;

ex b

for n, m being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines PairFunc NAGATA_2:def 1 :

for b_{1} being Function of [:NAT,NAT:],NAT holds

( b_{1} = PairFunc iff for n, m being Nat holds b_{1} . [n,m] = ((2 |^ n) * ((2 * m) + 1)) - 1 );

for b

( b

definition

let X be set ;

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

let x be Element of X;

ex b_{1} being Function of X,REAL st

for y being Element of X holds b_{1} . y = f . (x,y)

for b_{1}, b_{2} being Function of X,REAL st ( for y being Element of X holds b_{1} . y = f . (x,y) ) & ( for y being Element of X holds b_{2} . y = f . (x,y) ) holds

b_{1} = b_{2}

end;
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 for y being Element of X holds it . y = f . (x,y);

ex b

for y being Element of X holds b

proof end;

uniqueness for b

b

proof 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_{4} being Function of X,REAL holds

( b_{4} = dist (f,x) iff for y being Element of X holds b_{4} . y = f . (x,y) );

for X being set

for f being Function of [:X,X:],REAL

for x being Element of X

for b

( b

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 ) )

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

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;

ex b_{1} being Function of X,REAL st

for x being Element of X holds b_{1} . x = lower_bound ((dist (f,x)) .: A)

for b_{1}, b_{2} being Function of X,REAL st ( for x being Element of X holds b_{1} . x = lower_bound ((dist (f,x)) .: A) ) & ( for x being Element of X holds b_{2} . x = lower_bound ((dist (f,x)) .: A) ) holds

b_{1} = b_{2}

end;
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 for x being Element of X holds it . x = lower_bound ((dist (f,x)) .: A);

ex b

for x being Element of X holds b

proof end;

uniqueness for b

b

proof 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 b_{4} being Function of X,REAL holds

( b_{4} = lower_bound (f,A) iff for x being Element of X holds b_{4} . x = lower_bound ((dist (f,x)) .: A) );

for X being non empty set

for f being Function of [:X,X:],REAL

for A being Subset of X

for b

( b

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

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

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)

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

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

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

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

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)

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

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

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 ) )

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

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 )

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)) )

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 ;

:: 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 )

( ( 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 )

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

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 )

( ( 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;