:: The {N}agata-Smirnov Theorem. {P}art {I} :: by Karol P\c{a}k :: :: Received May 31, 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, XBOOLE_0, PRE_TOPC, METRIC_1, REAL_1, XXREAL_0, CARD_1, ARYTM_3, COMPLEX1, ARYTM_1, SETFAM_1, NATTRA_1, RCOMP_1, SUBSET_1, STRUCT_0, TARSKI, ZFMISC_1, PCOMPS_1, FINSET_1, FUNCT_1, CARD_3, FUNCOP_1, COMPTS_1, RELAT_1, ORDINAL1, RLVECT_3, CARD_5, NEWTON, FINSEQ_1, PSCOMP_1, ORDINAL2, TOPMETR, TMAP_1, BINOP_1, FUNCT_2, SETWISEO, COH_SP, FINSOP_1, NAT_1, RELAT_2, NAGATA_1, FUNCT_7; notations BINOP_1, SETWISEO, TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, ORDINAL1, COMPLEX1, RELSET_1, FUNCT_2, FINSEQ_1, ZFMISC_1, PCOMPS_1, PRE_TOPC, FINSET_1, CARD_1, XCMPLX_0, NUMBERS, XXREAL_0, XREAL_0, REAL_1, NAT_1, FINSOP_1, VALUED_1, STRUCT_0, TOPS_2, COMPTS_1, METRIC_1, NEWTON, CARD_3, PROB_1, FUNCOP_1, CANTOR_1, DOMAIN_1, TOPMETR, PSCOMP_1, BORSUK_1, TMAP_1; constructors SETWISEO, REAL_1, PROB_1, FUNCOP_1, FINSOP_1, NEWTON, CARD_5, TOPS_2, COMPTS_1, TMAP_1, CANTOR_1, PCOMPS_1, PSCOMP_1, URYSOHN3, BINOP_1; registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, CARD_LAR, STRUCT_0, TOPS_1, COMPTS_1, METRIC_1, BORSUK_1, TOPMETR, PSCOMP_1, VALUED_0, VALUED_1, FUNCT_2, CARD_3, FUNCT_1, PRE_TOPC, ZFMISC_1, BINOP_2, NEWTON, ORDINAL1; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin reserve T, T1 for non empty TopSpace; definition let T be TopSpace; let F be Subset-Family of T; attr F is discrete means :: NAGATA_1:def 1 for p being Point of T ex O being open Subset of T st p in O & for A,B being Subset of T st A in F & B in F holds O meets A & O meets B implies A=B; end; registration let T be non empty TopSpace; cluster discrete for Subset-Family of T; end; registration let T; cluster empty discrete for Subset-Family of T; end; reserve F,G,H for Subset-Family of T, A,B,C,D for Subset of T, O,U for open Subset of T, p,q for Point of T, x,y,X for set; theorem :: NAGATA_1:1 for F st (ex A st F={A}) holds F is discrete; theorem :: NAGATA_1:2 for F,G st F c= G & G is discrete holds F is discrete; theorem :: NAGATA_1:3 for F,G st F is discrete holds F/\G is discrete; theorem :: NAGATA_1:4 for F,G st F is discrete holds F\G is discrete; theorem :: NAGATA_1:5 for F,G,H st F is discrete & G is discrete & INTERSECTION(F,G)=H holds H is discrete; theorem :: NAGATA_1:6 for F,A,B st F is discrete & A in F & B in F holds A=B or A misses B; theorem :: NAGATA_1:7 F is discrete implies for p ex O st p in O & INTERSECTION({O},F)\ {{}} is trivial; theorem :: NAGATA_1:8 F is discrete iff (for p ex O st p in O & INTERSECTION({O},F)\{{}} is trivial) & for A,B st A in F & B in F holds A=B or A misses B; registration let T; let F be discrete Subset-Family of T; cluster clf F -> discrete; end; theorem :: NAGATA_1:9 for F st F is discrete holds for A,B st A in F & B in F holds Cl(A/\B) =Cl A /\ Cl B; theorem :: NAGATA_1:10 for F st F is discrete holds Cl union(F) = union (clf F); theorem :: NAGATA_1:11 for F st F is discrete holds F is locally_finite; definition let T be TopSpace; mode FamilySequence of T is sequence of bool bool(the carrier of T) qua non empty set; end; reserve Un for FamilySequence of T, r,r1,r2 for Real, n for Element of NAT; definition let T,Un,n; redefine func Un.n -> Subset-Family of T; end; definition let T,Un; redefine func Union Un ->Subset-Family of T; end; definition let T be non empty TopSpace; let Un be FamilySequence of T; attr Un is sigma_discrete means :: NAGATA_1:def 2 for n being Element of NAT holds Un.n is discrete; end; registration let T be non empty TopSpace; cluster sigma_discrete for FamilySequence of T; end; definition let T be non empty TopSpace; let Un be FamilySequence of T; attr Un is sigma_locally_finite means :: NAGATA_1:def 3 for n being Element of NAT holds Un.n is locally_finite; end; definition let T; let F be Subset-Family of T; attr F is sigma_discrete means :: NAGATA_1:def 4 ex f being sigma_discrete FamilySequence of T st F = Union f; end; registration let T be non empty TopSpace; cluster sigma_locally_finite for FamilySequence of T; end; theorem :: NAGATA_1:12 for Un st Un is sigma_discrete holds Un is sigma_locally_finite; theorem :: NAGATA_1:13 for A being uncountable set ex F being Subset-Family of 1TopSp([:A,A:] ) st F is locally_finite & F is not sigma_discrete; definition let T be non empty TopSpace; let Un be FamilySequence of T; attr Un is Basis_sigma_discrete means :: NAGATA_1:def 5 Un is sigma_discrete & Union Un is Basis of T; end; definition let T be non empty TopSpace; let Un be FamilySequence of T; attr Un is Basis_sigma_locally_finite means :: NAGATA_1:def 6 Un is sigma_locally_finite & Union Un is Basis of T; end; theorem :: NAGATA_1:14 for r being Real, PM be non empty MetrSpace for x being Element of PM holds [#]PM\cl_Ball(x,r) in Family_open_set(PM); theorem :: NAGATA_1:15 for T st T is metrizable holds T is regular & T is T_1; theorem :: NAGATA_1:16 for T st T is metrizable ex Un being FamilySequence of T st Un is Basis_sigma_locally_finite; theorem :: NAGATA_1:17 for U being sequence of bool(the carrier of T) st (for n holds U.n is open) holds Union U is open; theorem :: NAGATA_1:18 (for A,U st A is closed & U is open & A c=U ex W being sequence of bool(the carrier of T) st A c= Union W & Union W c= U & (for n holds Cl (W.n) c= U & W.n is open )) implies T is normal; theorem :: NAGATA_1:19 for T st T is regular for Bn being FamilySequence of T st (Union Bn) is Basis of T holds for U being Subset of T,p being Point of T st U is open & p in U ex O being Subset of T st p in O & Cl O c= U & O in Union Bn; theorem :: NAGATA_1:20 for T st T is regular & ex Bn being FamilySequence of T st Bn is Basis_sigma_locally_finite holds T is normal; definition let T; let F,G be RealMap of T; redefine func F+G -> RealMap of T means :: NAGATA_1:def 7 for t being Element of T holds it.t=F.t+G.t; end; theorem :: NAGATA_1:21 for f being RealMap of T st f is continuous for F being RealMap of [:T ,T:] st for x,y being Element of T holds F.(x,y)=|.f.x-f.y.| holds F is continuous; theorem :: NAGATA_1:22 for F,G being RealMap of T st F is continuous & G is continuous holds F + G is continuous; theorem :: NAGATA_1:23 for ADD being BinOp of Funcs(the carrier of T,REAL) st (for f1, f2 being RealMap of T holds ADD.(f1,f2)=f1+f2) holds ADD is having_a_unity & ADD is commutative associative; theorem :: NAGATA_1:24 for ADD being BinOp of Funcs(the carrier of T,REAL) st (for f1, f2 being RealMap of T holds ADD.(f1,f2)=f1+f2) for map9 being Element of Funcs( the carrier of T,REAL) st map9 is_a_unity_wrt ADD holds map9 is continuous; definition let A,B be non empty set; let F be Function of A,Funcs(A,B); func F Toler -> Function of A,B means :: NAGATA_1:def 8 for p be Element of A holds it. p=F.p.p; end; theorem :: NAGATA_1:25 for ADD being BinOp of Funcs(the carrier of T,REAL) st (for f1,f2 being RealMap of T holds ADD.(f1,f2)=f1+f2) for F being FinSequence of Funcs( the carrier of T,REAL) st for n st 0 <> n & n <= len F holds F.n is continuous RealMap of T holds ADD "**" F is continuous RealMap of T; theorem :: NAGATA_1:26 for F be Function of the carrier of T,Funcs(the carrier of T,the carrier of T1) st for p be Point of T holds F.p is continuous Function of T,T1 for S be Function of the carrier of T,bool the carrier of T st for p be Point of T holds p in S.p & S.p is open & for p,q be Point of T st p in S.q holds F.p .p=F.q.p holds F Toler is continuous; reserve m for Function of [:the carrier of T,the carrier of T:],REAL; definition let X,r; let f be Function of X,REAL; func min(r,f) -> Function of X,REAL means :: NAGATA_1:def 9 for x st x in X holds it.x = min(r,f.x); end; theorem :: NAGATA_1:27 for r be Real,f be RealMap of T st f is continuous holds min(r,f) is continuous; definition let X be set, f be Function of [:X,X:],REAL; pred f is_a_pseudometric_of X means :: NAGATA_1:def 10 f is Reflexive symmetric triangle; end; theorem :: NAGATA_1:28 for f be Function of [:X,X:],REAL holds f is_a_pseudometric_of X iff for a,b,c be Element of X holds f.(a,a) = 0 & f.(a,c)<=f.(a,b)+f.(c,b); theorem :: NAGATA_1:29 for f be Function of [:X,X:],REAL st f is_a_pseudometric_of X for x,y be Element of X holds f.(x,y)>=0; theorem :: NAGATA_1:30 for r,m st r>0 & m is_a_pseudometric_of (the carrier of T) holds min(r,m) is_a_pseudometric_of (the carrier of T); theorem :: NAGATA_1:31 for r,m st r>0 & m is_metric_of (the carrier of T) holds min(r,m) is_metric_of (the carrier of T);