:: 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
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, REAL_1, XBOOLE_0, PRE_TOPC, ZFMISC_1,
STRUCT_0, FUNCT_1, PSCOMP_1, SEQFUNC, SEQ_1, XXREAL_0, CARD_1, NEWTON,
RELAT_1, ARYTM_3, INT_1, NAT_1, ARYTM_1, FUNCT_7, FUNCT_2, TARSKI,
METRIC_1, RCOMP_1, MCART_1, SETFAM_1, ORDINAL2, TOPMETR, TMAP_1, SEQ_4,
NAGATA_1, XXREAL_2, COMPLEX1, RELAT_2, VALUED_0, PCOMPS_1, PBOOLE,
SERIES_1, CARD_3, VALUED_1, SEQ_2, FINSEQ_1, PREPOWER, BINOP_1, SETWISEO,
FINSOP_1, ORDINAL4, CARD_5, RLVECT_3, FINSET_1, COH_SP, PARTFUN1,
WELLORD1, PCOMPS_2, NATTRA_1, NAGATA_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, SETWISEO, BORSUK_1,
RELAT_1, RELAT_2, ORDINAL1, XCMPLX_0, XXREAL_0, XXREAL_2, XREAL_0,
FUNCT_1, COMPLEX1, REAL_1, RELSET_1, PARTFUN1, VALUED_0, VALUED_1, SEQ_1,
FUNCT_2, FUNCT_3, DOMAIN_1, BINOP_1, PRE_TOPC, NAT_1, NAT_D, CARD_1,
NUMBERS, FINSET_1, STRUCT_0, FINSEQ_1, PCOMPS_1, PCOMPS_2, NEWTON,
TOPS_2, METRIC_1, PROB_1, SEQFUNC, PREPOWER, TOPMETR, PSCOMP_1, TMAP_1,
NAGATA_1, SEQ_2, SEQ_4, SERIES_1, FINSOP_1, CANTOR_1, WELLORD1, FUNCT_7;
constructors WELLORD1, FUNCT_3, SETWISEO, REAL_1, NAT_D, PROB_1, FINSOP_1,
NEWTON, PREPOWER, SERIES_1, FUNCT_7, TOPS_2, TMAP_1, CANTOR_1, PCOMPS_2,
NAGATA_1, BORSUK_4, SEQFUNC, SEQ_4, BINOP_2, SEQ_2, PSCOMP_1, PCOMPS_1,
COMSEQ_2, BINOP_1, URYSOHN3, SUPINF_2;
registrations SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XXREAL_0,
XREAL_0, NAT_1, MEMBERED, FINSEQ_1, STRUCT_0, TOPS_1, METRIC_1, BORSUK_1,
TOPMETR, TOPREAL6, VALUED_0, VALUED_1, FUNCT_2, CARD_1, PRE_TOPC,
FUNCT_1, PSCOMP_1, NEWTON, BINOP_2;
requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM;
begin
reserve i, k, m, n for Nat,
r, s for Real,
rn for Real,
x, y , z, X for set,
T, T1, T2 for non empty TopSpace,
p, q for Point of T,
A, B, C for Subset of T,
A9 for non empty Subset of T,
pq for Element of [:the carrier of T,the carrier of T:],
pq9 for Point of [:T,T:],
pmet,pmet1 for Function of [:the carrier of T,the carrier of T:],REAL,
pmet9,pmet19 for RealMap of [:T,T:] ,
f,f1 for RealMap of T,
FS2 for Functional_Sequence of [:the carrier of T,the carrier of T:],REAL,
seq for Real_Sequence;
theorem :: NAGATA_2:1
for i st i>0 ex n,m st i=(2|^n)*(2*m+1);
definition
func PairFunc -> Function of [:NAT,NAT:],NAT means
:: NAGATA_2:def 1
for n,m holds it.[ n,m] = (2|^n)*(2*m+1)-1;
end;
theorem :: NAGATA_2:2
PairFunc is bijective;
definition
let X be set,f be Function of [:X,X:],REAL,x be Element of X;
func dist(f,x) -> Function of X,REAL means
:: NAGATA_2:def 2
for y be Element of X holds it.y = f.(x,y);
end;
theorem :: NAGATA_2:3
for D be Subset of [:T1,T2:] st D is open for x1 be Point of T1,
x2 be Point of T2 for X1 be Subset of T1,X2 be 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);
theorem :: NAGATA_2:4
for pmet st for pmet9 st pmet=pmet9 holds pmet9 is continuous for
x be Point of T holds dist(pmet,x) is continuous;
definition
let X be non empty set,f be Function of [:X,X:],REAL,A be Subset of X;
func lower_bound(f,A) -> Function of X,REAL means
:: NAGATA_2:def 3
for x be Element of X holds it.x = lower_bound((dist(f,x)).:A);
end;
theorem :: NAGATA_2:5
for X be non empty set,f be Function of [:X,X:],REAL st f
is_a_pseudometric_of X for A be non empty Subset of X,x be Element of X holds
lower_bound(f,A).x>=0;
theorem :: NAGATA_2:6
for X be non empty set,f be Function of [:X,X:],REAL st f
is_a_pseudometric_of X for A be Subset of X,x be Element of X holds x in A
implies lower_bound(f,A).x=0;
theorem :: NAGATA_2:7
for pmet st pmet is_a_pseudometric_of the carrier of T for x,y be
Point of T,A be non empty Subset of T
holds |.lower_bound(pmet,A).x-lower_bound(pmet,A).y.|<=
pmet.(x,y);
theorem :: NAGATA_2:8
for pmet st pmet is_a_pseudometric_of the carrier of T & for p
holds dist(pmet,p) is continuous for A be non empty Subset of T
holds lower_bound(pmet,
A) is continuous;
theorem :: NAGATA_2:9
for f be Function of [:X,X:],REAL st f is_metric_of X holds f
is_a_pseudometric_of X;
theorem :: NAGATA_2:10
for pmet st pmet is_metric_of the carrier of T & (for A be 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;
theorem :: NAGATA_2:11
for FS2 st (for n ex pmet st FS2.n=pmet & pmet
is_a_pseudometric_of the carrier of T) & for pq holds FS2#pq is summable for
pmet st for pq holds pmet.pq=Sum(FS2#pq) holds pmet is_a_pseudometric_of the
carrier of T;
theorem :: NAGATA_2:12
for n,seq st for m st m<=n holds seq.m<=r for m st m<=n holds
Partial_Sums(seq).m <= r * (m+1);
theorem :: NAGATA_2:13
for k holds |.Partial_Sums(seq).k.|<=Partial_Sums(abs(seq)).k;
theorem :: NAGATA_2:14
for FS1 being Functional_Sequence of the carrier of T,REAL st (
for n ex f st FS1.n=f & f is continuous & for p holds f.p>=0) & (ex seq st seq
is summable & for n,p holds (FS1#p).n<=seq.n) for f st for p holds f.p=Sum(FS1#
p) holds f is continuous;
theorem :: NAGATA_2:15
for s, FS2 st for n ex pmet st FS2.n=pmet & pmet
is_a_pseudometric_of the carrier of T & (for pq holds pmet.pq<=s) & for pmet9
st pmet=pmet9 holds pmet9 is continuous for pmet st for pq holds pmet.pq=Sum((1
/2)GeoSeq(#)(FS2#pq)) holds pmet is_a_pseudometric_of the carrier of T & for
pmet9 st pmet=pmet9 holds pmet9 is continuous;
theorem :: NAGATA_2:16
for pmet st pmet is_a_pseudometric_of the carrier of T & for
pmet9 st pmet=pmet9 holds pmet9 is continuous for A be non empty Subset of T,p
holds p in Cl A implies lower_bound(pmet,A).p=0;
theorem :: NAGATA_2:17
for T st T is T_1 for s, FS2 st (for n ex pmet st FS2.n=pmet &
pmet is_a_pseudometric_of the carrier of T & (for pq holds pmet.pq<=s) & for
pmet9 st pmet=pmet9 holds pmet9 is continuous) & for p,A9 st not p in A9 & A9
is closed ex n st for pmet st FS2.n=pmet holds lower_bound(pmet,A9).p>0
holds (ex pmet
st pmet is_metric_of the carrier of T & for pq holds pmet.pq=Sum((1/2)GeoSeq(#)
(FS2#pq))) & T is metrizable;
theorem :: NAGATA_2:18
for D being non empty set, p,q be FinSequence of D,B be BinOp of
D st p is one-to-one & q is one-to-one & rng q c= rng p & B is commutative
associative & (B is having_a_unity or len q>=1 & len p>len q) holds ex r be
FinSequence of D st r is one-to-one & rng r=rng p \rng q & B "**" p =B.(B "**"
q,B "**" r);
::$N Nagata-Smirnov metrization theorem
theorem :: NAGATA_2:19
for T 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;
theorem :: NAGATA_2:20
T is metrizable implies for FX be Subset-Family of T st FX is
Cover of T & FX is open ex Un be FamilySequence of T st Union Un is open &
Union Un is Cover of T & Union Un is_finer_than FX & Un is sigma_discrete;
theorem :: NAGATA_2:21
for T st T is metrizable ex Un be FamilySequence of T st Un is
Basis_sigma_discrete;
::$N Bing metrization theorem
theorem :: NAGATA_2:22
for T holds (T is regular & T is T_1 & ex Bn being FamilySequence of T
st Bn is Basis_sigma_discrete) iff T is metrizable;