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