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