:: The {N}agata-Smirnov Theorem. {P}art {II}
:: by Karol P\c{a}k
::
:: Received July 22, 2004
:: Copyright (c) 2004-2026 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;
definitions FUNCT_2, TARSKI, TOPS_2, XBOOLE_0, XXREAL_2;
equalities XBOOLE_0, BINOP_1, SUBSET_1, STRUCT_0;
expansions FUNCT_2, TARSKI, TOPS_2, XBOOLE_0, BINOP_1, XXREAL_2;
theorems NAT_1, NEWTON, FUNCT_2, PCOMPS_1, PCOMPS_2, NAGATA_1, SUBSET_1,
METRIC_6, FUNCT_3, FUNCT_1, METRIC_1, XCMPLX_1, ABSVALUE, TOPMETR,
TMAP_1, BORSUK_1, XBOOLE_1, TARSKI, SETFAM_1, XBOOLE_0, TOPS_1, TOPS_2,
PRE_TOPC, FINSEQ_1, CARD_4, ZFMISC_1, BINOP_1, SEQ_2, SEQ_4, SEQ_1,
SERIES_1, PREPOWER, SEQFUNC, PARTFUN1, JGRAPH_2, URYSOHN1, FINSEQ_3,
FINSEQ_4, FINSOP_1, SETWISEO, PROB_1, URYSOHN3, WELLORD1, WELLORD2,
TBSP_1, RELAT_1, RELAT_2, YELLOW_9, RSSPACE2, RSSPACE, BHSP_5, XREAL_1,
COMPLEX1, XXREAL_0, ORDINAL1, NAT_D, VALUED_1, JORDAN5A, XTUPLE_0,
XREAL_0;
schemes FUNCT_2, NAT_1, SEQFUNC, FRAENKEL, BINOP_1, PCOMPS_2;
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 Th1:
for i st i>0 ex n,m st i=(2|^n)*(2*m+1)
proof
defpred N[Nat] means
for k st 1<=k & k<=$1 ex n,m st k=(2|^n)*(2*m+1);
A1: for i st N[i] holds N[i + 1]
proof
let i such that
A2: N[i];
let k such that
A3: 1<=k and
A4: k <=i+1;
now
per cases by A4,XXREAL_0:1;
suppose
A5: k=i+1 & i=0;
set m=0;
A6: 1=2|^0 by NEWTON:4;
k=1*(m*2+1) by A5;
hence thesis by A6;
end;
suppose
A7: k=i+1 & i>0;
per cases by NAT_D:12;
suppose
k mod 2=1;
then consider m being Nat such that
A8: k = 2 * m + 1 and
1<2 by NAT_D:def 2;
reconsider m as Element of NAT by ORDINAL1:def 12;
1=2|^0 by NEWTON:4;
then k=(2|^0)*(2*m+1) by A8;
hence thesis;
end;
suppose
k mod 2=0;
then consider j being Nat such that
A9: k = 2 * j + 0 and
0<2 by NAT_D:def 2;
reconsider j as Element of NAT by ORDINAL1:def 12;
A10: j<=i
proof
assume j>i;
then j+j>i+1 by NAT_1:14,XREAL_1:8;
hence thesis by A7,A9;
end;
j<>0 by A7,A9;
then j>=1 by NAT_1:14;
then consider n,m such that
A11: j=(2|^n)*(2*m+1) by A2,A10;
k=(2*(2|^n))*(2*m+1) by A9,A11;
then k=(2|^(n+1))*(2*m+1) by NEWTON:6;
hence thesis;
end;
end;
suppose
k<i+1;
then k<=i by NAT_1:13;
hence thesis by A2,A3;
end;
end;
hence thesis;
end;
let i;
assume i>0;
then
A12: i>=1 by NAT_1:14;
A13: N[ 0 ];
for n holds N[n] from NAT_1:sch 2(A13,A1);
hence thesis by A12;
end;
definition
func PairFunc -> Function of [:NAT,NAT:],NAT means
:Def1:
for n,m holds it.[ n,m] = (2|^n)*(2*m+1)-1;
existence
proof
deffunc N(Element of NAT,Element of NAT) = In((2|^$1)*(2*$2+1)-1,NAT);
A1: for n,m be Element of NAT holds (2|^n)*(2*m+1)-1 in NAT
proof
let n,m be Element of NAT;
0 < 2|^n by NEWTON:83;
then ((2|^n)*(2*m+1))-1 is Element of NAT by NAT_1:20,XREAL_1:129;
hence thesis;
end;
consider NN being Function of [:NAT,NAT:],NAT such that
A2: for n,m being Element of NAT holds NN.(n,m) = N(n,m) from BINOP_1:
sch 4;
take NN;
let n,m;
A3: n in NAT & m in NAT by ORDINAL1:def 12;
NN.(n,m) = In((2|^n)*(2*m+1)-1,NAT) by A2,A3
.= (2|^n)*(2*m+1)-1 by A1,SUBSET_1:def 8,A3;
hence thesis;
end;
uniqueness
proof
let N1,N2 be Function of [:NAT,NAT:],NAT;
assume that
A4: for n,m holds N1.[n,m] = (2|^n)*(2*m+1)-1 and
A5: for n,m holds N2.[n,m] = (2|^n)*(2*m+1)-1;
now
let n,m be Element of NAT;
N1.[n,m] = (2|^n)*(2*m+1)-1 by A4;
hence N1.(n,m)=N2.(n,m) by A5;
end;
hence thesis;
end;
end;
theorem Th2:
PairFunc is bijective
proof
now
let nm1,nm2 be object;
assume that
A1: nm1 in [:NAT,NAT:] and
A2: nm2 in [:NAT,NAT:] and
A3: PairFunc.nm1=PairFunc.nm2;
consider n2,m2 be object such that
A4: n2 in NAT & m2 in NAT and
A5: [n2,m2]=nm2 by A2,ZFMISC_1:def 2;
consider n1,m1 be object such that
A6: n1 in NAT & m1 in NAT and
A7: [n1,m1]=nm1 by A1,ZFMISC_1:def 2;
reconsider n1,n2,m1,m2 as Element of NAT by A6,A4;
A8: (2|^n2)*(2*m2+1)-1=PairFunc.nm2 by A5,Def1;
A9: (2|^n1)*(2*m1+1)-1=PairFunc.nm1 by A7,Def1;
then n1=n2 by A3,A8,CARD_4:4;
hence nm1=nm2 by A3,A7,A5,A9,A8,CARD_4:4;
end;
hence PairFunc is one-to-one by FUNCT_2:19;
now
let i be object;
assume
i in NAT;
then reconsider i9=i as Element of NAT;
consider n, m be Nat such that
A10: i9+1=(2|^n) *(2*m+1) by Th1;
n in NAT & m in NAT by ORDINAL1:def 12;
then
A11: [n,m] in [:NAT,NAT:] by ZFMISC_1:87;
i9-0=((2|^n) *(2*m+1))-1 by A10;
then dom PairFunc = [:NAT,NAT:] & i= PairFunc.[n,m] by Def1,FUNCT_2:def 1;
hence i in rng PairFunc by FUNCT_1:def 3,A11;
end;
then NAT c= rng PairFunc;
then NAT=rng PairFunc;
hence PairFunc is onto;
end;
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
:Def2:
for y be Element of X holds it.y = f.(x,y);
existence
proof
deffunc D(object)=f.(x,$1);
A1: for y being object st y in X holds D(y) in REAL
by XREAL_0:def 1;
consider DIST be Function of X,REAL such that
A2: for y being object st y in X holds DIST.y =D(y)
from FUNCT_2:sch 2(A1);
now
per cases;
suppose
A3: X is empty;
let y be Element of X;
not [x,y] in dom f by A3;
then
A4: f.[x,y]={} by FUNCT_1:def 2;
not y in dom DIST by A3;
hence f.(x,y)=DIST.y by A4,FUNCT_1:def 2;
end;
suppose
X is non empty;
hence for y be Element of X holds DIST.y = f.(x,y) by A2;
end;
end;
hence thesis;
end;
uniqueness
proof
let D1,D2 be Function of X,REAL;
assume that
A5: for y be Element of X holds D1.y=f.(x,y) and
A6: for y be Element of X holds D2.y=f.(x,y);
now
let y be Element of X;
D1.y=f.(x,y) by A5;
hence D1.y=D2.y by A6;
end;
hence thesis;
end;
end;
theorem Th3:
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)
proof
set cT1 =the carrier of T1;
set cT2=the carrier of T2;
let D be Subset of [:T1,T2:];
assume D is open;
then consider FA be Subset-Family of [:T1,T2:] such that
A1: D=union FA and
A2: for B be set st B in FA ex B1 being Subset of T1, B2 being Subset of
T2 st B = [:B1,B2:] & B1 is open & B2 is open by BORSUK_1:5;
let x1 be Point of T1, x2 be Point of T2;
let X1 be Subset of T1,X2 be Subset of T2;
thus X1=pr1(cT1,cT2).:(D/\[:cT1,{x2}:]) implies X1 is open
proof
assume
A3: X1=pr1(cT1,cT2).:(D/\[:cT1,{x2}:]);
for t be set holds t in X1 iff ex U be Subset of T1 st U is open & U
c= X1 & t in U
proof
let t be set;
t in X1 implies ex U be Subset of T1 st U is open & U c= X1 & t in U
proof
assume t in X1;
then consider tx be object such that
A4: tx in dom pr1(cT1,cT2) and
A5: tx in (D/\[:cT1,{x2}:]) and
A6: t=pr1(cT1,cT2).tx by A3,FUNCT_1:def 6;
tx in D by A5,XBOOLE_0:def 4;
then consider tX be set such that
A7: tx in tX and
A8: tX in FA by A1,TARSKI:def 4;
consider tX1 be Subset of T1,tX2 be Subset of T2 such that
A9: tX=[:tX1,tX2:] and
A10: tX1 is open and
tX2 is open by A2,A8;
take tX1;
thus tX1 is open by A10;
consider tx1,tx2 be object such that
A11: tx1 in cT1 & tx2 in cT2 and
A12: tx=[tx1,tx2] by A4,ZFMISC_1:def 2;
thus tX1 c=X1
proof
tx in [:cT1,{x2}:] by A5,XBOOLE_0:def 4;
then
A13: tx2=x2 by A12,ZFMISC_1:106;
let a be object such that
A14: a in tX1;
[a,x2] in [:cT1,cT2:] by A14,ZFMISC_1:87;
then
A15: [a,x2] in dom pr1(cT1,cT2) by FUNCT_3:def 4;
tx2 in tX2 by A12,A7,A9,ZFMISC_1:87;
then [a,x2] in [:tX1,tX2:] by A14,A13,ZFMISC_1:87;
then
A16: [a,x2] in union FA by A8,A9,TARSKI:def 4;
[a,x2] in [:cT1,{x2}:] by A14,ZFMISC_1:106;
then [a,x2] in D/\[:cT1,{x2}:] by A1,A16,XBOOLE_0:def 4;
then pr1(cT1,cT2).(a,x2) in pr1(cT1,cT2).:(D/\[:cT1,{x2}:]) by A15,
FUNCT_1:def 6;
hence thesis by A3,A14,FUNCT_3:def 4;
end;
pr1(cT1,cT2).(tx1,tx2)=tx1 by A11,FUNCT_3:def 4;
hence thesis by A6,A12,A7,A9,ZFMISC_1:87;
end;
hence thesis;
end;
hence thesis by TOPS_1:25;
end;
thus X2= pr2(cT1,cT2).:(D/\[:{x1},cT2:]) implies X2 is open
proof
assume
A17: X2=pr2(cT1,cT2).:(D/\[:{x1},cT2:]);
for t be set holds t in X2 iff ex U be Subset of T2 st U is open & U
c= X2 & t in U
proof
let t be set;
t in X2 implies ex U be Subset of T2 st U is open & U c= X2 & t in U
proof
assume t in X2;
then consider tx be object such that
A18: tx in dom pr2(cT1,cT2) and
A19: tx in (D/\[:{x1},cT2:]) and
A20: t=pr2(cT1,cT2).tx by A17,FUNCT_1:def 6;
tx in D by A19,XBOOLE_0:def 4;
then consider tX be set such that
A21: tx in tX and
A22: tX in FA by A1,TARSKI:def 4;
consider tx1,tx2 be object such that
A23: tx1 in cT1 & tx2 in cT2 and
A24: tx=[tx1,tx2] by A18,ZFMISC_1:def 2;
A25: pr2(cT1,cT2).(tx1,tx2)=tx2 by A23,FUNCT_3:def 5;
consider tX1 be Subset of T1,tX2 be Subset of T2 such that
A26: tX=[:tX1,tX2:] and
tX1 is open and
A27: tX2 is open by A2,A22;
A28: tX2 c=X2
proof
tx in [:{x1},cT2:] by A19,XBOOLE_0:def 4;
then
A29: tx1=x1 by A24,ZFMISC_1:105;
let a be object such that
A30: a in tX2;
[x1,a] in [:cT1,cT2:] by A30,ZFMISC_1:87;
then
A31: [x1,a] in dom pr2(cT1,cT2) by FUNCT_3:def 5;
tx1 in tX1 by A24,A21,A26,ZFMISC_1:87;
then [x1,a] in [:tX1,tX2:] by A30,A29,ZFMISC_1:87;
then
A32: [x1,a] in union FA by A22,A26,TARSKI:def 4;
[x1,a] in [:{x1},cT2:] by A30,ZFMISC_1:105;
then [x1,a] in D/\[:{x1},cT2:] by A1,A32,XBOOLE_0:def 4;
then pr2(cT1,cT2).(x1,a) in pr2(cT1,cT2).:(D/\[:{x1},cT2:]) by A31,
FUNCT_1:def 6;
hence thesis by A17,A30,FUNCT_3:def 5;
end;
tx2 in tX2 by A24,A21,A26,ZFMISC_1:87;
hence thesis by A20,A24,A27,A25,A28;
end;
hence thesis;
end;
hence thesis by TOPS_1:25;
end;
end;
theorem Th4:
for pmet st for pmet9 st pmet=pmet9 holds pmet9 is continuous for
x be Point of T holds dist(pmet,x) is continuous
proof
set cT=the carrier of T;
let pmet such that
A1: for pmet9 st pmet=pmet9 holds pmet9 is continuous;
[:cT,cT:]= the carrier of [:T,T:] by BORSUK_1:def 2;
then reconsider pmet9=pmet as RealMap of [:T,T:];
reconsider pmetR=pmet9 as Function of [:T,T:],R^1 by TOPMETR:17;
let x be Point of T;
reconsider distx=dist(pmet,x) as Function of T,R^1 by TOPMETR:17;
pmet9 is continuous by A1;
then
A2: pmetR is continuous by JORDAN5A:27;
now
let t be Point of T;
for R being Subset of R^1 st R is open & distx.t in R ex U being
Subset of T st U is open & t in U & distx.:U c= R
proof
reconsider xt=[x,t] as Point of [:T,T:] by BORSUK_1:def 2;
A3: dom pr2(cT,cT)=[:cT,cT:] by FUNCT_3:def 5;
A4: pmetR is_continuous_at xt & distx.t=pmet.(x,t) by A2,Def2,TMAP_1:50;
let R be Subset of R^1;
assume R is open & distx.t in R;
then consider XU be Subset of [:T,T:] such that
A5: XU is open and
A6: xt in XU and
A7: pmetR.:XU c= R by A4,TMAP_1:43;
set U=pr2(cT,cT).:(XU/\[:{x},cT:]);
[x,t] in [:{x},cT:] by ZFMISC_1:105;
then [x,t] in XU/\[:{x},cT:] by A6,XBOOLE_0:def 4;
then pr2(cT,cT).(x,t) in pr2(cT,cT).:(XU/\[:{x},cT:]) by A3,FUNCT_1:def 6
;
then
A8: t in U by FUNCT_3:def 5;
A9: distx.:U c= R
proof
let du be object;
assume du in distx.:U;
then consider u be object such that
A10: u in dom distx and
A11: u in U and
A12: distx.u=du by FUNCT_1:def 6;
reconsider u as Point of T by A10;
consider xu be object such that
A13: xu in dom pr2(cT,cT) and
A14: xu in (XU/\[:{x},cT:]) and
A15: pr2(cT,cT).xu=u by A11,FUNCT_1:def 6;
consider x9,u9 be object such that
A16: x9 in cT & u9 in cT and
A17: xu=[x9,u9] by A13,ZFMISC_1:def 2;
reconsider x9,u9 as Point of T by A16;
[x9,u9] in [:{x},cT:] by A14,A17,XBOOLE_0:def 4;
then pr2(cT,cT).(x9,u9) = u9 & x9=x by FUNCT_3:def 5,ZFMISC_1:105;
then
A18: pmet.(x9,u9)=du by A12,A15,A17,Def2;
A19: dom pmetR=the carrier of [:T,T:] by FUNCT_2:def 1;
[x9,u9] in XU by A14,A17,XBOOLE_0:def 4;
then du in pmetR.:XU by A18,A19,FUNCT_1:def 6;
hence thesis by A7;
end;
U is open by A5,Th3;
hence thesis by A8,A9;
end;
hence distx is_continuous_at t by TMAP_1:43;
end;
then distx is continuous by TMAP_1:50;
hence thesis by JORDAN5A:27;
end;
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
:Def3:
for x be Element of X holds it.x = lower_bound((dist(f,x)).:A);
existence
proof
deffunc I(Element of X)= In(lower_bound((dist(f,$1)).:A),REAL);
consider INF be Function of X,REAL such that
A1: for x being Element of X holds INF.x = I(x) from FUNCT_2:sch 4;
take INF;
let x be Element of X;
INF.x = I(x) by A1;
hence thesis;
end;
uniqueness
proof
let I1,I2 be Function of X,REAL;
assume that
A2: for x be Element of X holds I1.x=lower_bound((dist(f,x)).:A) and
A3: for x be Element of X holds I2.x=lower_bound((dist(f,x)).:A);
now
let x be Element of X;
I1.x=lower_bound((dist(f,x)).:A) by A2;
hence I1.x=I2.x by A3;
end;
hence thesis;
end;
end;
Lm1: for X be non empty set,f be Function of [:X,X:],REAL st f
is_a_pseudometric_of X holds f is bounded_below & for A be non empty Subset of
X,x be Element of X holds dist(f,x).:A is non empty bounded_below
proof
let X be non empty set,f be Function of [:X,X:],REAL such that
A1: f is_a_pseudometric_of X;
A2: now
let A be non empty Subset of X,x be Element of X;
A3: 0 is LowerBound of dist(f,x).:A
proof
let rn be ExtReal;
assume rn in dist(f,x).:A;
then consider y being object such that
A4: y in dom dist(f,x) and
y in A and
A5: rn = dist(f,x).y by FUNCT_1:def 6;
reconsider y as Element of X by A4;
f.(x,y)>=0 by A1,NAGATA_1:29;
hence rn>=0 by A5,Def2;
end;
dom dist(f,x)=X by FUNCT_2:def 1;
hence dist(f,x).:A is non empty bounded_below by A3;
end;
now
let xy be object;
assume xy in dom f;
then consider x,y being object such that
A6: x in X & y in X and
A7: [x,y] = xy by ZFMISC_1:def 2;
reconsider x,y as Element of X by A6;
f.(x,y) >=0 & 0>-1 by A1,NAGATA_1:29;
hence f.xy>-1 by A7;
end;
hence thesis by A2,SEQ_2:def 2;
end;
theorem Th5:
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
proof
let X be non empty set,f be Function of [:X,X:],REAL such that
A1: f is_a_pseudometric_of X;
let A be non empty Subset of X,x be Element of X;
A2: now
let rn;
assume rn in (dist(f,x)).:A;
then consider y being object such that
A3: y in dom dist(f,x) and
y in A and
A4: rn = dist(f,x).y by FUNCT_1:def 6;
dist(f,x).y=f.(x,y) by A3,Def2;
hence rn>=0 by A1,A3,A4,NAGATA_1:29;
end;
X=dom dist(f,x) by FUNCT_2:def 1;
then lower_bound ((dist(f,x)).:A)>=0 by A2,SEQ_4:43;
hence thesis by Def3;
end;
theorem Th6:
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
proof
let X be non empty set,f be Function of [:X,X:],REAL such that
A1: f is_a_pseudometric_of X;
let A be Subset of X,x be Element of X;
assume
A2: x in A;
then reconsider A as non empty Subset of X;
A3: dist(f,x).:A is non empty bounded_below by A1,Lm1;
f is Reflexive by A1,NAGATA_1:def 10;
then f.(x,x)=0 by METRIC_1:def 2;
then X=dom dist(f,x) & dist(f,x).x=0 by Def2,FUNCT_2:def 1;
then 0 in dist(f,x).:A by A2,FUNCT_1:def 6;
then lower_bound(dist(f,x).:A)<=0 by A3,SEQ_4:def 2;
then lower_bound(f,A).x <=0 by Def3;
hence thesis by A1,Th5;
end;
theorem Th7:
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)
proof
let pmet such that
A1: pmet is_a_pseudometric_of the carrier of T;
A2: pmet is symmetric by A1,NAGATA_1:def 10;
let x,y be Point of T,A be non empty Subset of T;
A3: for x1,y1 be Point of T
holds lower_bound(pmet,A).y1-lower_bound(pmet,A).x1>=-pmet.(x1,
y1)
proof
let x1,y1 be Point of T;
A4: dist(pmet,x1).:A is non empty bounded_below by A1,Lm1;
A5: for rn st rn in dist(pmet,y1).:A
holds rn>=lower_bound(dist(pmet,x1).:A)-pmet.
(x1,y1)
proof
let rn;
assume rn in dist(pmet,y1).:A;
then consider z being object such that
A6: z in dom dist(pmet,y1) and
A7: z in A and
A8: dist(pmet,y1).z=rn by FUNCT_1:def 6;
reconsider z as Point of T by A6;
A9: dist(pmet,x1).z= pmet.(x1,z) by Def2;
pmet is triangle by A1,NAGATA_1:def 10;
then
A10: pmet.(x1,y1)+pmet.(y1,z)>=pmet.(x1,z) by METRIC_1:def 5;
dom dist(pmet,x1)= the carrier of T by FUNCT_2:def 1;
then dist(pmet,x1).z in dist(pmet,x1).:A by A7,FUNCT_1:def 6;
then pmet.(x1,z)>=lower_bound(dist(pmet,x1).:A) by A4,A9,SEQ_4:def 2;
then pmet.(x1,y1)+pmet.(y1,z)>=lower_bound(dist(pmet,x1).:A)+0
by A10,XXREAL_0:2;
then pmet.(y1,z)-0>=lower_bound(dist(pmet,x1).:A)-pmet.(x1,y1)
by XREAL_1:21;
hence thesis by A8,Def2;
end;
dist(pmet,y1).:A is non empty bounded_below by A1,Lm1;
then lower_bound(dist(pmet,y1).:A)-0>=
lower_bound(dist(pmet,x1).:A)-pmet.(x1,y1) by A5,SEQ_4:43;
then
A11: lower_bound(dist(pmet,y1).:A)-lower_bound(dist(pmet,x1).:A)
>=0-pmet.(x1,y1) by XREAL_1:17;
lower_bound(dist(pmet,y1).:A)=lower_bound(pmet,A).y1 by Def3;
hence thesis by A11,Def3;
end;
then lower_bound(pmet,A).y-lower_bound(pmet,A).x>=-pmet.(x,y);
then -(lower_bound(pmet,A).x-lower_bound(pmet,A).y)>=-pmet.(x,y);
then
A12: (lower_bound(pmet,A).x-lower_bound(pmet,A).y)<= pmet.(x,y) by XREAL_1:24;
lower_bound(pmet,A).x-lower_bound(pmet,A).y>=-pmet.(y,x) by A3;
then (lower_bound(pmet,A).x-lower_bound(pmet,A).y)>=-pmet.(x,y)
by A2,METRIC_1:def 4;
hence thesis by A12,ABSVALUE:5;
end;
theorem Th8:
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
proof
let pmet such that
A1: pmet is_a_pseudometric_of the carrier of T and
A2: for p holds dist(pmet,p) is continuous;
let A be non empty Subset of T;
reconsider infR=lower_bound(pmet,A) as Function of T,R^1 by TOPMETR:17;
now
let t be Point of T;
reconsider dR=dist(pmet,t) as Function of T,R^1 by TOPMETR:17;
for R being Subset of R^1 st R is open & infR.t in R ex U being Subset
of T st U is open & t in U & infR.:U c= R
proof
reconsider infRt=infR qua real-valued Function.t, dRt=dR qua real-valued
Function.t as Point of RealSpace by METRIC_1:def 13, XREAL_0:def 1;
let R be Subset of R^1;
assume R is open & infR.t in R;
then consider r being Real such that
A3: r>0 and
A4: Ball(infRt,r) c= R by TOPMETR:15,def 6;
reconsider dB=Ball(dRt,r) as Subset of R^1 by METRIC_1:def 13,TOPMETR:17;
|.dR.t-dR.t.|=0 by ABSVALUE:2;
then dist(dRt,dRt)<r by A3,TOPMETR:11;
then
A5: dRt in dB by METRIC_1:11;
dist(pmet,t) is continuous by A2;
then dR is continuous by JORDAN5A:27;
then dB is open & dR is_continuous_at t by TMAP_1:50,TOPMETR:14,def 6;
then consider B be Subset of T such that
A6: B is open & t in B and
A7: dR.:B c=dB by A5,TMAP_1:43;
infR.:B c= R
proof
let Ib be object;
assume Ib in infR.:B;
then consider b be object such that
A8: b in dom infR and
A9: b in B and
A10: infR.b=Ib by FUNCT_1:def 6;
reconsider b as Point of T by A8;
reconsider infRb=infR qua real-valued Function.b, dRb=dR qua
real-valued Function.b as Point of RealSpace
by METRIC_1:def 13,XREAL_0:def 1;
pmet.(t,b)>=0 by A1,NAGATA_1:29;
then
A11: dR.b>=0 by Def2;
dR.t=pmet.(t,t) by Def2;
then dR.t=0 by A1,NAGATA_1:28;
then
A12: dist(dRt,dRb)=|.0-dR.b.| by TOPMETR:11;
dom dR=the carrier of T by FUNCT_2:def 1;
then dR.b in dR.:B by A9,FUNCT_1:def 6;
then dist(dRt,dRb)<r by A7,METRIC_1:11;
then |.-(0-dR.b).|<r by A12,COMPLEX1:52;
then dR.b<r by A11,ABSVALUE:def 1;
then
A13: pmet.(t,b) < r by Def2;
|.lower_bound(pmet,A).t-lower_bound(pmet,A).b.|<=pmet.(t,b) &
dist(infRt,infRb)=
|.lower_bound( pmet,A).t-lower_bound(pmet,A).b.| by A1,Th7,TOPMETR:11;
then dist(infRt,infRb)<r by A13,XXREAL_0:2;
then infRb in Ball(infRt,r) by METRIC_1:11;
hence thesis by A4,A10;
end;
hence thesis by A6;
end;
hence infR is_continuous_at t by TMAP_1:43;
end;
then infR is continuous by TMAP_1:50;
hence thesis by JORDAN5A:27;
end;
theorem Th9:
for f be Function of [:X,X:],REAL st f is_metric_of X holds f
is_a_pseudometric_of X
proof
let f be Function of [:X,X:],REAL;
assume f is_metric_of X;
then
for a,b,c be Element of X holds f.(a,a)=0 & f.(a,b)=f.(b,a) & f.(a,c)<=f
.(a,b)+f.(b,c) by PCOMPS_1:def 6;
then f is Reflexive symmetric triangle by METRIC_1:def 2,def 4,def 5;
hence thesis by NAGATA_1:def 10;
end;
theorem Th10:
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
proof
let pmet such that
A1: pmet is_metric_of the carrier of T and
A2: for A be non empty Subset of T holds Cl A={p where p is Point of T:
lower_bound(pmet,A).p=0};
set PM=SpaceMetr(the carrier of T,pmet);
reconsider PM as non empty MetrSpace by A1,PCOMPS_1:36;
A3: for x,y be Element of PM holds pmet.(x,y)=dist(x,y)
proof
let x,y be Element of PM;
PM=MetrStruct(#the carrier of T,pmet#) by A1,PCOMPS_1:def 7;
hence thesis by METRIC_1:def 1;
end;
A4: Family_open_set PM c= the topology of T
proof
let A be object;
assume
A5: A in Family_open_set PM;
then reconsider AT=A as Subset of T by A1,PCOMPS_2:4;
per cases;
suppose
AT` is empty;
then AT`=([#]T)` by XBOOLE_1:37;
then AT=the carrier of T by TOPS_1:1;
hence thesis by PRE_TOPC:def 1;
end;
suppose
A6: AT` is non empty;
for x holds x in AT iff ex U be Subset of T st U is open & U c= AT
& x in U
proof
let x;
x in AT implies ex U be Subset of T st U is open & U c= AT & x in U
proof
assume
A7: x in AT;
then reconsider xP=x as Element of PM by A1,PCOMPS_2:4;
consider r such that
A8: r>0 and
A9: Ball(xP,r) c= AT by A5,A7,PCOMPS_1:def 4;
reconsider xT=x as Element of T by A7;
A10: ex y being object st y in AT` by A6;
reconsider B=Ball(xP,r) as Subset of T by A1,PCOMPS_2:4;
set Inf={p where p is Point of T:lower_bound(pmet,B`).p=0};
AT`c=B` by A9,SUBSET_1:12;
then consider b be set such that
A11: b in B` by A10;
B`=Inf
proof
thus B`c=Inf
proof
let y be object such that
A12: y in B`;
lower_bound(pmet,B`).y=0 by A1,A12,Th6,Th9;
hence thesis by A12;
end;
let y be object;
assume y in Inf;
then consider yT be Point of T such that
A13: y=yT and
A14: lower_bound(pmet,B`).yT=0;
assume not y in B`;
then
A15: yT in B by A13,XBOOLE_0:def 5;
reconsider yP=yT as Point of PM by A1,PCOMPS_2:4;
pmet is_a_pseudometric_of the carrier of T by A1,Th9;
then
A16: dist(pmet,yT).:B` is non empty bounded_below by A11,Lm1;
Ball(xP,r) in Family_open_set PM by PCOMPS_1:29;
then consider s such that
A17: s>0 and
A18: Ball(yP,s)c=Ball(xP,r) by A15,PCOMPS_1:def 4;
lower_bound(dist(pmet,yT).:B`)=0 by A14,Def3;
then consider rn such that
A19: rn in dist(pmet,yT).:B` and
A20: rn<0+s by A17,A16,SEQ_4:def 2;
consider z being object such that
A21: z in dom dist(pmet,yT) and
A22: z in B` and
A23: rn =dist(pmet,yT).z by A19,FUNCT_1:def 6;
reconsider zT=z as Point of T by A21;
reconsider zP=z as Point of PM by A1,A21,PCOMPS_2:4;
pmet.(yT,zT)<s by A20,A23,Def2;
then dist(yP,zP)<s by A3;
then zP in Ball(yP,s) by METRIC_1:11;
then B` meets B by A18,A22,XBOOLE_0:3;
hence thesis by XBOOLE_1:79;
end;
then B`=Cl B` by A2,A11;
then
A24: B is open by TOPS_1:4;
pmet.(xT,xT)=0 by A1,PCOMPS_1:def 6;
then dist(xP,xP)<r by A3,A8;
then xP in B by METRIC_1:11;
hence thesis by A9,A24;
end;
hence thesis;
end;
then AT is open by TOPS_1:25;
hence thesis by PRE_TOPC:def 2;
end;
end;
the topology of T c=Family_open_set PM
proof
let A be object;
assume
A25: A in the topology of T;
then reconsider AT=A as Subset of T;
reconsider AP=A as Subset of PM by A1,A25,PCOMPS_2:4;
per cases;
suppose
AT` is empty;
then AT`=([#]T)` by XBOOLE_1:37;
then AT=the carrier of T by TOPS_1:1;
then AT=the carrier of PM by A1,PCOMPS_2:4;
hence thesis by PCOMPS_1:30;
end;
suppose
A26: AT` is non empty;
for xP be Element of PM st xP in AP holds ex r st r>0 & Ball(xP,r) c= AP
proof
let xP be Element of PM such that
A27: xP in AP;
reconsider xT=xP as Element of T by A1,PCOMPS_2:4;
take r=lower_bound(pmet,AT`).xT;
A28: Ball(xP,r) c= AP
proof
pmet is_a_pseudometric_of the carrier of T by A1,Th9;
then
A29: dist(pmet,xT).:AT` is non empty bounded_below by A26,Lm1;
let y be object;
assume that
A30: y in Ball(xP,r) and
A31: not y in AP;
reconsider yP=y as Point of PM by A30;
A32: dist(xP,yP)<r by A30,METRIC_1:11;
reconsider yT=yP as Point of T by A1,PCOMPS_2:4;
A33: dom dist(pmet,xT) = the carrier of T by FUNCT_2:def 1;
yT in AT` by A31,XBOOLE_0:def 5;
then dist(pmet,xT).yT in dist(pmet,xT).:AT` by A33,FUNCT_1:def 6;
then
A34: lower_bound(dist(pmet,xT).:AT`)<=dist(pmet,xT).yT by A29,SEQ_4:def 2;
dist(pmet,xT).yT=pmet.(xT,yT) & lower_bound(dist(pmet,xT).:AT`)
= lower_bound(
pmet,AT`).xT by Def2,Def3;
hence thesis by A3,A32,A34;
end;
AT is open by A25,PRE_TOPC:def 2;
then AT`=Cl AT` by PRE_TOPC:22;
then
A35: AT`={p where p is Point of T:lower_bound(pmet,AT`).p=0} by A2,A26;
lower_bound(pmet,AT`).xT>0
proof
assume lower_bound(pmet,AT`).xT<=0;
then lower_bound(pmet,AT`).xT=0 by A1,A26,Th5,Th9;
then xT in AT` by A35;
then AT` meets AT by A27,XBOOLE_0:3;
hence thesis by XBOOLE_1:79;
end;
hence thesis by A28;
end;
hence thesis by PCOMPS_1:def 4;
end;
end;
then the topology of T =Family_open_set PM by A4;
hence thesis by A1,PCOMPS_1:def 8;
end;
theorem Th11:
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
proof
set cT=the carrier of T;
let FS2 such that
A1: for n ex pmet st FS2.n=pmet & pmet is_a_pseudometric_of cT and
A2: for pq holds FS2#pq is summable;
let pmet such that
A3: for pq holds pmet.pq=Sum(FS2#pq);
now
let a,b,c be Point of T;
thus pmet.(a,a)=0
proof
set aa=[a,a];
set F=FS2#aa;
now
let n;
consider pmet1 such that
A4: FS2.n=pmet1 and
A5: pmet1 is_a_pseudometric_of cT by A1;
pmet1.(a,a)=0 by A5,NAGATA_1:28;
hence F.n=0*F.n by A4,SEQFUNC:def 10;
end;
then
A6: F=0(#)F by SEQ_1:9;
F is summable by A2;
then Sum(F)=0*Sum(F) by A6,SERIES_1:10;
hence thesis by A3;
end;
thus pmet.(a,c)<=pmet.(a,b)+pmet.(c,b)
proof
set ab=[a,b],cb=[c,b],ac=[a,c];
set Fac=FS2#ac;
set Fab=FS2#ab;
set Fcb=FS2#cb;
A7: now
let n;
A8: FS2.n.ac= Fac.n & FS2.n.ab=Fab.n by SEQFUNC:def 10;
consider pmet1 such that
A9: FS2.n=pmet1 and
A10: pmet1 is_a_pseudometric_of cT by A1;
A11: 0<=pmet1.(a,c) by A10,NAGATA_1:29;
pmet1.(a,c)<=pmet1.(a,b)+pmet1.(c,b) by A10,NAGATA_1:28;
then Fac.n<=(Fab.n+Fcb.n) by A9,A8,SEQFUNC:def 10;
hence 0<=Fac.n & Fac.n<=(Fab+Fcb).n
by A9,A11,SEQFUNC:def 10,SEQ_1:7;
end;
A12: Fab is summable & Fcb is summable by A2;
then Fab+Fcb is summable by SERIES_1:7;
then
A13: Sum(Fac)<=Sum(Fab+Fcb) by A7,SERIES_1:20;
A14: Sum(Fab)=pmet.ab & Sum(Fcb)=pmet.cb by A3;
Sum(Fab+Fcb)=Sum(Fab)+Sum(Fcb) by A12,SERIES_1:7;
hence thesis by A3,A13,A14;
end;
end;
hence thesis by NAGATA_1:28;
end;
theorem Th12:
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)
proof
let n,seq such that
A1: for m st m<=n holds seq.m<=r;
defpred P[Nat] means
$1<=n implies Partial_Sums(seq).$1<=r*($1+1);
A2: for m st P[m] holds P[m+1]
proof
let m such that
A3: P[m];
A4: Partial_Sums(seq).(m+1) = Partial_Sums(seq).m+seq.(m+1) by SERIES_1:def 1;
assume
A5: m+1<=n;
then seq.(m+1)<=r by A1;
then Partial_Sums(seq).(m+1)<=(r*(m+1)) + r by A3,A5,A4,NAT_1:13,XREAL_1:7;
hence thesis;
end;
Partial_Sums(seq).0=seq.0 by SERIES_1:def 1;
then
A6: P[ 0 ] by A1;
for m holds P[m] from NAT_1:sch 2(A6,A2);
hence thesis;
end;
theorem Th13:
for k holds |.Partial_Sums(seq).k.|<=Partial_Sums(abs(seq)).k
proof
set PS=Partial_Sums(seq),absPS=Partial_Sums(abs(seq));
defpred P[Nat] means |.PS.$1.|<=absPS.$1;
A1: for k st P[k] holds P[k+1]
proof
let k;
assume P[k];
then
A2: |.PS.k.|+|.seq.(k+1).| <=absPS.k+|.seq.(k+1).| by XREAL_1:7;
PS.(k+1)=PS.k+seq.(k+1) by SERIES_1:def 1;
then
A3: |.PS.(k+1).|<=|.PS.k.|+|.seq.(k+1).| by COMPLEX1:56;
(abs seq).(k+1)= |.seq.(k+1).| by SEQ_1:12;
then |.PS.(k+1).|<=absPS.k+(abs seq).(k+1) by A3,A2,XXREAL_0:2;
hence thesis by SERIES_1:def 1;
end;
absPS.0=(abs seq).0 & (abs seq).0=|.seq.0 .| by SEQ_1:12,SERIES_1:def 1;
then
A4: P[ 0 ] by SERIES_1:def 1;
for k holds P[k] from NAT_1:sch 2(A4,A1);
hence thesis;
end;
theorem Th14:
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
proof
let FS1 be Functional_Sequence of the carrier of T,REAL such that
A1: for n ex f st FS1.n=f & f is continuous & for p holds f.p>=0 and
A2: ex seq st seq is summable & for n,p holds (FS1#p).n<=seq.n;
let f such that
A3: for p holds f.p=Sum(FS1#p);
reconsider fR=f as Function of T,R^1 by TOPMETR:17;
now
let p;
for R being Subset of R^1 st R is open & fR.p in R ex U being Subset
of T st U is open & p in U & fR.:U c= R
proof
reconsider fRp=fR qua real-valued Function.p as Point of RealSpace by
METRIC_1:def 13,XREAL_0:def 1;
let R be Subset of R^1;
assume R is open & fR.p in R;
then consider rn such that
A4: rn>0 and
A5: Ball(fRp,rn) c= R by TOPMETR:15,def 6;
set r2=rn/2,r4=rn/4;
reconsider r2,r4 as Real;
A6: r4>0 by A4,XREAL_1:224;
consider seq such that
A7: seq is summable and
A8: for n,q holds (FS1#q).n<=seq.n by A2;
Partial_Sums(seq) is convergent by A7,SERIES_1:def 2;
then consider n such that
A9: for m st n<=m holds |.Partial_Sums(seq).m-lim Partial_Sums(
seq).|<r4 by A6,SEQ_2:def 7;
defpred Sn[object,object] means
ex SS being Subset of T st SS = $2 & SS is
open & p in SS & for f1 st FS1.$1=f1 for f1p be Point of RealSpace st f1p=f1.p
holds f1.:SS c= Ball(f1p,r2/(n+1));
A10: for k being object st k in {0}\/Seg(n)
ex U be object st U in bool the carrier of T & Sn[k,U]
proof
let k be object;
assume k in {0}\/Seg(n);
then k in Seg(n) or k in {0} by XBOOLE_0:def 3;
then reconsider k as Element of NAT by TARSKI:def 1;
consider f1 such that
A11: FS1.k=f1 and
A12: f1 is continuous and
for p holds f1.p>=0 by A1;
reconsider f19=f1 as Function of T,R^1 by TOPMETR:17;
reconsider f1p=f19 qua real-valued Function.p as Point of RealSpace by
METRIC_1:def 13,XREAL_0:def 1;
set B=Ball(f1p,r2/(n+1));
reconsider B as Subset of R^1 by METRIC_1:def 13,TOPMETR:17;
dist(f1p,f1p)=0 & r2>0 by A4,METRIC_1:1,XREAL_1:215;
then dist(f1p,f1p)<r2/(n+1) by XREAL_1:139;
then
A13: f1p in B by METRIC_1:11;
f19 is continuous by A12,JORDAN5A:27;
then B is open & f19 is_continuous_at p by TMAP_1:50,TOPMETR:14,def 6;
then consider U be Subset of T such that
A14: U is open & p in U and
A15: f19.:U c= B by A13,TMAP_1:43;
for f1 st FS1.k=f1 for f1p be Point of RealSpace st f1p=f1.p
holds f1.:U c= Ball(f1p,r2/(n+1)) by A11,A15;
hence thesis by A14;
end;
consider FSn be Function of ({0}\/Seg(n)),bool the carrier of T such
that
A16: for k being object st k in {0}\/Seg(n) holds Sn[k,FSn.k] from
FUNCT_2:sch 1(A10);
A17: for k,q holds (FS1#q).k>=0
proof
let k,q;
(ex f1 st FS1.k=f1 & f1 is continuous & for q holds f1.q >=0 )&
FS1.k.q=( FS1#q).k by A1,SEQFUNC:def 10;
hence thesis;
end;
A18: for k holds (seq^\(n+1)).k>=0
proof
let k;
0<=(FS1#p).(n+1+k) & seq.(n+1+k)=(seq^\(n+1)).k by A17,NAT_1:def 3;
hence thesis by A8;
end;
reconsider RNG=rng FSn as Subset-Family of T;
A19: RNG is open
proof
let Q be Subset of T;
assume Q in RNG;
then consider x being object such that
A20: x in dom FSn and
A21: FSn.x=Q by FUNCT_1:def 3;
ex SS being Subset of T st SS = FSn.x & SS is open & p in SS & for
f1 st FS1.x=f1 for f1p be Point of RealSpace st f1p=f1.p holds f1 .:SS c= Ball(
f1p,r2/(n+1)) by A16,A20;
hence thesis by A21;
end;
0 in {0} by TARSKI:def 1;
then 0 in {0}\/Seg(n) by XBOOLE_0:def 3;
then reconsider RNG as non empty Subset-Family of T by FUNCT_2:4;
A22: lim Partial_Sums( seq ) =Sum(seq) & Sum(seq)=Partial_Sums(seq).n +
Sum(seq^\ (n+1)) by A7,SERIES_1:15,def 3;
|.Partial_Sums(seq).n-lim Partial_Sums(seq).|<r4 by A9;
then |.-Sum(seq^\(n+1)).|<r4 by A22;
then
A23: |.Sum(seq^\(n+1)).|<r4 by COMPLEX1:52;
seq^\(n+1) is summable by A7,SERIES_1:12;
then Sum(seq^\(n+1))>=0 by A18,SERIES_1:18;
then
A24: Sum(seq^\(n+1))<r4 by A23,ABSVALUE:def 1;
A25: for q holds FS1#q is summable & 0<=Sum((FS1#q)^\(n+1)) & Sum((FS1#q
)^\(n+1))<r4
proof
let q;
set F=FS1#q;
A26: now
let k;
A27: seq.(n+1+k)= (seq^\(n+1)).k by NAT_1:def 3;
0<=F.(n+1+k) & F.(n+1+k)<=seq.(n+1+k) by A8,A17;
hence 0<=(F^\(n+1)).k & (F^\(n+1)).k<=(seq^\(n+1)).k by A27,
NAT_1:def 3;
end;
A28: for k holds 0<=F.k & F.k<=seq.k by A8,A17;
then F is summable by A7,SERIES_1:20;
then
A29: F^\(n+1) is summable by SERIES_1:12;
seq^\(n+1) is summable by A7,SERIES_1:12;
then Sum(F^\(n+1))<=Sum(seq^\(n+1)) by A26,SERIES_1:20;
hence thesis by A7,A24,A28,A26,A29,SERIES_1:18,20,XXREAL_0:2;
end;
A30: fR.:(meet RNG)c=R
proof
let fRq be object;
assume fRq in fR.:(meet RNG);
then consider q be object such that
A31: q in dom fR and
A32: q in meet RNG and
A33: fRq=fR.q by FUNCT_1:def 6;
reconsider q as Point of T by A31;
set sp=FS1#p, sq=FS1#q, spn=sp^\(n+1), sqn=sq^\(n+1);
set absPSpq=Partial_Sums(|.sp-sq.|);
for k st k<=n holds (|.sp-sq.|).k <=r2/(n+1)
proof
let k such that
A34: k<=n;
k=0 or k>=1 by NAT_1:14;
then k in {0} or k in Seg n by A34,FINSEQ_1:1,TARSKI:def 1;
then
A35: k in {0}\/Seg n by XBOOLE_0:def 3;
then FSn.k in RNG by FUNCT_2:4;
then
A36: q in FSn.k by A32,SETFAM_1:def 1;
A37: k in NAT by ORDINAL1:def 12;
dom (sp-sq)= NAT by FUNCT_2:def 1;
then
A38: (sp-sq).k=sp.k-sq.k by VALUED_1:13,A37;
consider f1 such that
A39: FS1.k=f1 and
f1 is continuous and
for p holds f1.p>=0 by A1;
reconsider f1p=f1.p,f1q=f1.q as Point of RealSpace by METRIC_1:def 13
;
ex SS being Subset of T st SS = FSn.k & SS is open & p in SS &
for f1 st FS1.k=f1 for f1p be Point of RealSpace st f1p=f1.p holds f1 .:SS c=
Ball(f1p,r2/(n+1)) by A16,A35;
then
A40: f1.:(FSn.k) c= Ball(f1p,r2/(n+1)) by A39;
dom f1=the carrier of T by FUNCT_2:def 1;
then f1q in f1.:(FSn.k) by A36,FUNCT_1:def 6;
then dist(f1p,f1q)<r2/(n+1) by A40,METRIC_1:11;
then
A41: |.f1.p-f1.q.|<r2/(n+1) by TOPMETR:11;
f1.p=sp.k by A39,SEQFUNC:def 10;
then |.sp.k-sq.k.|<r2/(n+1) by A39,A41,SEQFUNC:def 10;
hence thesis by A38,SEQ_1:12;
end;
then
A42: absPSpq.n <=(r2/(n+1))*(n+1) by Th12;
A43: n in NAT by ORDINAL1:def 12;
set PSp=Partial_Sums(sp),PSq=Partial_Sums(sq),PSpq=Partial_Sums(sp-sq);
PSp-PSq=PSpq & dom (PSp-PSq)= NAT by SEQ_1:1,SERIES_1:6;
then
A44: |.PSp.n-PSq.n.|=|.PSpq.n.| by VALUED_1:13,A43;
|.PSpq.n.|<=absPSpq.n by Th13;
then |.PSp.n-PSq.n.|<=(r2/(n+1))*(n+1) by A44,A42,XXREAL_0:2;
then
A45: |.PSp.n-PSq.n.|<=r2 by XCMPLX_1:87;
0<=Sum(spn) by A25;
then
A46: |.Sum(spn).|=Sum(spn) by ABSVALUE:def 1;
0<=Sum(sqn) by A25;
then
A47: |.Sum(sqn).|=Sum(sqn) by ABSVALUE:def 1;
reconsider fRq=fR qua real-valued Function.q as Point of RealSpace by
METRIC_1:def 13,XREAL_0:def 1;
A48: |.Sum(spn)-Sum(sqn).|<=|.Sum(spn).|+|.Sum(sqn).| by COMPLEX1:57;
A49: fRp=Sum(sp) & fRq=Sum(sq) by A3;
Sum(sp)=PSp.n+Sum(spn) & Sum(sq)=PSq.n+Sum(sqn) by A25,SERIES_1:15;
then |.fR.p-fR.q.| =|.(PSp.n-PSq.n)+(Sum(spn)-Sum(sqn)).| by A49;
then
A50: |.fR.p-fR.q.|<=|.PSp.n-PSq.n.|+|.Sum(spn)-Sum(sqn).| by COMPLEX1:56;
Sum(spn)<r4 & Sum(sqn)<r4 by A25;
then |.Sum(spn).|+|.Sum(sqn).|<r4+r4 by A46,A47,XREAL_1:8;
then |.Sum(spn)-Sum(sqn).|<r2 by A48,XXREAL_0:2;
then |.PSp.n-PSq.n.|+|.Sum(spn)-Sum(sqn).|<r2+r2 by A45,XREAL_1:8;
then |.fR.p-fR.q.|<rn by A50,XXREAL_0:2;
then dist(fRp,fRq)<rn by TOPMETR:11;
then fRq in Ball(fRp,rn) by METRIC_1:11;
hence thesis by A5,A33;
end;
now
let Fx be set;
assume Fx in RNG;
then consider x being object such that
A51: x in dom FSn and
A52: FSn.x=Fx by FUNCT_1:def 3;
ex SS being Subset of T st SS = FSn.x & SS is open & p in SS & for
f1 st FS1.x=f1 for f1p be Point of RealSpace st f1p=f1.p holds f1 .:SS c= Ball(
f1p,r2/(n+1)) by A16,A51;
hence p in Fx by A52;
end;
then p in meet RNG by SETFAM_1:def 1;
hence thesis by A19,A30,TOPS_2:20;
end;
hence fR is_continuous_at p by TMAP_1:43;
end;
then fR is continuous by TMAP_1:50;
hence thesis by JORDAN5A:27;
end;
theorem Th15:
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
proof
set Geo=(1/2)GeoSeq;
set cT=the carrier of T,cTT= the carrier of [:T,T:];
let s, FS2 such that
A1: for n ex pmet st FS2.n=pmet & pmet is_a_pseudometric_of cT & (for pq
holds pmet.pq<=s) & for pmet9 st pmet=pmet9 holds pmet9 is continuous;
set SGeo=s(#)(Geo);
deffunc GF(Nat)=(Geo.$1)(#)(FS2.$1);
consider GeoF be Functional_Sequence of [:cT,cT:],REAL such that
A2: for n be Nat holds GeoF.n = GF(n) from SEQFUNC:sch 1;
cTT = [:cT,cT:] by BORSUK_1:def 2;
then reconsider GeoF9=GeoF as Functional_Sequence of cTT,REAL;
A3: for pq,k holds 0<=(GeoF#pq).k & (GeoF#pq).k<=SGeo.k
proof
let pq,k;
consider x,y being object such that
A4: x in cT & y in cT and
A5: [x,y]=pq by ZFMISC_1:def 2;
reconsider x,y as Point of T by A4;
consider pmet1 such that
A6: FS2.k=pmet1 and
A7: pmet1 is_a_pseudometric_of cT and
A8: for pq holds pmet1.pq<=s and
for pmet19 st pmet1=pmet19 holds pmet19 is continuous by A1;
A9: 0<=pmet1.(x,y) by A7,NAGATA_1:29;
dom ((Geo.k)(#)(FS2.k))=[:cT,cT:] by A6,FUNCT_2:def 1;
then
A10: (Geo.k)*(FS2.k).pq=((Geo.k)(#)(FS2.k)).pq by VALUED_1:def 5
.=GeoF.k.pq by A2
.=(GeoF#pq).k by SEQFUNC:def 10;
(1/2)|^k>0 by NEWTON:83;
then
A11: Geo.k>0 by PREPOWER:def 1;
then (Geo.k)*(pmet1.pq)<=(Geo.k)*s by A8,XREAL_1:64;
hence thesis by A6,A5,A10,A9,A11,SEQ_1:9;
end;
A12: for n ex f be RealMap of [:T,T:] st (GeoF9.n=f & f is continuous & for
pq9 holds f.pq9>=0)
proof
let n;
consider pmet1 such that
A13: FS2.n=pmet1 and
pmet1 is_a_pseudometric_of cT and
for pq holds pmet1.pq<=s and
A14: for pmet19 st pmet1=pmet19 holds pmet19 is continuous by A1;
cTT=[:cT,cT:] by BORSUK_1:def 2;
then reconsider pmet19=pmet1 as RealMap of [:T,T:];
reconsider pR=pmet19 as Function of [:T,T:],R^1 by TOPMETR:17;
pmet19 is continuous by A14;
then pR is continuous by JORDAN5A:27;
then consider fR be Function of [:T,T:],R^1 such that
A15: for pq9 be Point of [:T,T:],rn st pR.pq9=rn holds fR.pq9= (Geo.n) *rn and
A16: fR is continuous by JGRAPH_2:23;
reconsider f=fR as RealMap of [:T,T:] by TOPMETR:17;
A17: dom f=cTT by FUNCT_2:def 1;
take f;
A18: dom pmet1=[:cT,cT:] by FUNCT_2:def 1;
A19: (GeoF9.n)=(Geo.n)(#)FS2.n by A2;
then
A20: dom (FS2.n)=dom (GeoF9.n) by VALUED_1:def 5;
A21: [:cT,cT:]=cTT by BORSUK_1:def 2;
A22: now
let pq9 such that
pq9 in dom (GeoF9.n);
(GeoF9.n).pq9=(Geo.n)*pmet1.pq9 by A13,A19,A20,A18,A21,VALUED_1:def 5;
hence (GeoF9.n).pq9=f.pq9 by A15;
end;
now
let pq9;
reconsider pq=pq9 as Element of [:cT,cT:] by BORSUK_1:def 2;
GeoF9.n.pq9=(GeoF#pq).n & (GeoF#pq).n >=0 by A3,SEQFUNC:def 10;
hence f.pq9>=0 by A13,A20,A18,A22;
end;
hence thesis by A13,A16,A20,A18,A17,A21,A22,JORDAN5A:27,PARTFUN1:5;
end;
let pmet such that
A23: for pq holds pmet.pq=Sum(Geo(#)(FS2#pq));
A24: for pq holds pmet.pq=Sum(GeoF#pq)
proof
let pq;
now
let z be object;
assume z in NAT;
then reconsider k=z as Element of NAT;
ex pmet1 st FS2.k=pmet1 & pmet1 is_a_pseudometric_of cT &( for pq
holds pmet1.pq<=s)& for pmet19 st pmet1=pmet19 holds pmet19 is continuous by A1
;
then dom ((Geo.k)(#)(FS2.k))=[:cT,cT:] by FUNCT_2:def 1;
then (Geo.k)*(FS2.k).pq=((Geo.k)(#)(FS2.k)).pq by VALUED_1:def 5
.=GeoF.k.pq by A2
.=(GeoF#pq).k by SEQFUNC:def 10;
then (GeoF#pq).k=(Geo.k)*(FS2#pq).k by SEQFUNC:def 10
.=(Geo(#)(FS2#pq)).k by SEQ_1:8;
hence (Geo(#)(FS2#pq)).z=(GeoF#pq).z;
end;
then Geo(#)(FS2#pq)=(GeoF#pq);
hence thesis by A23;
end;
A25: for n ex pmet1 st GeoF.n=pmet1 & pmet1 is_a_pseudometric_of cT
proof
let n;
consider pmet1 such that
A26: FS2.n=pmet1 and
A27: pmet1 is_a_pseudometric_of cT and
for pq holds pmet1.pq<=s and
for pmet19 st pmet1=pmet19 holds pmet19 is continuous by A1;
deffunc F(Element of cT,Element of cT)=(Geo.n)*pmet1.($1,$2);
consider GF be Function of [:cT,cT:],REAL such that
A28: for p for q holds GF.(p,q)=F(p,q) from BINOP_1:sch 4;
now
let a,b,c be Point of T;
(1/2)|^n>0 by NEWTON:83;
then
A29: ((1/2)GeoSeq.n)>0 by PREPOWER:def 1;
pmet1.(a,c)<=pmet1.(a,b)+pmet1.(c,b) by A27,NAGATA_1:28;
then pmet1.(a,c)*((1/2)GeoSeq.n)<=(pmet1.(a,b)+ pmet1.(c,b))*(Geo.n) by
A29,XREAL_1:64;
then
A30: GF.(a,c)<=(Geo.n)*pmet1.(a,b)+(Geo.n)*pmet1.(c,b) by A28;
GF.(a,a)=(Geo.n)*pmet1.(a,a) & pmet1.(a,a)=0 by A27,A28,NAGATA_1:28;
hence GF.(a,a)=0;
(Geo.n)*pmet1.(a,b)=GF.(a,b) by A28;
hence GF.(a,c)<=GF.(a,b)+GF.(c,b) by A28,A30;
end;
then
A31: GF is_a_pseudometric_of cT by NAGATA_1:28;
A32: (GeoF.n)=(Geo.n)(#)FS2.n by A2;
then
A33: dom (FS2.n)=dom (GeoF.n) by VALUED_1:def 5;
A34: now
let x,y be object;
assume
A35: [x,y] in dom (GeoF.n);
then reconsider x9=x,y9=y as Point of T by ZFMISC_1:87;
GF.(x9,y9)= (Geo.n)*pmet1.(x9,y9) by A28;
hence (GeoF.n).(x,y)=GF.(x,y) by A26,A32,A35,VALUED_1:def 5;
end;
dom pmet1=[:cT,cT:] & dom GF= [:cT,cT:] by FUNCT_2:def 1;
hence thesis by A26,A33,A34,A31,BINOP_1:20;
end;
(1/2)<1;
then |.1/2.|<1 by ABSVALUE:def 1;
then
A36: Geo is summable by SERIES_1:24;
A37: for pq,pq9 st pq=pq9 holds GeoF#pq=GeoF9#pq9
proof
let pq,pq9 such that
A38: pq=pq9;
now
let x be Element of NAT;
(GeoF#pq).x=GeoF.x.pq by SEQFUNC:def 10;
hence (GeoF#pq).x=(GeoF9#pq9).x by A38,SEQFUNC:def 10;
end;
hence thesis;
end;
A39: ex seq st seq is summable & for n,pq9 holds (GeoF9#pq9).n<=seq.n
proof
take SGeo;
thus SGeo is summable by A36,SERIES_1:10;
now
let n,pq9;
reconsider pq=pq9 as Element of [:cT,cT:] by BORSUK_1:def 2;
(GeoF9#pq9).n =(GeoF#pq).n by A37;
hence (GeoF9#pq9).n <=SGeo.n by A3;
end;
hence thesis;
end;
A40: for pmet19 st pmet=pmet19 holds pmet19 is continuous
by A12,A24,A39,Th14;
for pq holds GeoF#pq is summable
proof
let pq;
for k holds 0<=(GeoF#pq).k & (GeoF#pq).k<=SGeo.k & SGeo is summable
by A3,A36,SERIES_1:10;
hence thesis by SERIES_1:20;
end;
hence thesis by A25,A24,A40,Th11;
end;
theorem Th16:
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
proof
set rn=In(0,REAL);
let pmet such that
A1: pmet is_a_pseudometric_of the carrier of T and
A2: for pmet9 st pmet=pmet9 holds pmet9 is continuous;
let A be non empty Subset of T,p;
A3: dom lower_bound(pmet,A)= the carrier of T by FUNCT_2:def 1;
reconsider Z={rn},infA=lower_bound(pmet,A).:A as Subset of R^1 by TOPMETR:17;
infA c= Z
proof
let infa be object;
assume infa in infA;
then ex a be object st a in dom lower_bound(pmet,A) & a in A &
infa=lower_bound (pmet,A).a by FUNCT_1:def 6;
then infa=0 by A1,Th6;
hence thesis by TARSKI:def 1;
end;
then
A4: Cl (infA) c= Cl Z by PRE_TOPC:19;
reconsider InfA=lower_bound(pmet,A) as Function of T,R^1 by TOPMETR:17;
for p holds dist(pmet,p) is continuous by A2,Th4;
then lower_bound(pmet,A) is continuous by A1,Th8;
then InfA is continuous by JORDAN5A:27;
then
A5: InfA.:(Cl A) c= Cl(InfA.:A) by TOPS_2:45;
assume p in Cl A;
then
A6: lower_bound(pmet,A).p in lower_bound(pmet,A).:(Cl A) by A3,FUNCT_1:def 6;
Z is closed by PCOMPS_1:7,TOPMETR:17;
then Z=Cl Z by PRE_TOPC:22;
then InfA.:(Cl A)c=Z by A4,A5;
hence thesis by A6,TARSKI:def 1;
end;
theorem Th17:
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
proof
let T such that
A1: T is T_1;
set cT=the carrier of T,Geo=(1/2)GeoSeq;
let s,FS2 such that
A2: 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 and
A3: 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;
deffunc pm(Element of cT,Element of cT)=In(Sum(Geo(#)(FS2#[$1,$2])),REAL);
consider pmet such that
A4: for p,q holds pmet.(p,q)=pm(p,q) from BINOP_1:sch 4;
A5: for pq holds pmet.pq=Sum(Geo(#)(FS2#pq))
proof
let pq;
consider p,q be object such that
A6: p in cT & q in cT and
A7: pq=[p,q] by ZFMISC_1:def 2;
reconsider p,q as Element of cT by A6;
pmet.pq = pmet.(p,q) by A7
.= pm(p,q) by A4;
hence thesis by A7;
end;
A8: for pq,n holds 0<=(Geo(#)(FS2#pq)).n & (Geo(#)(FS2#pq)).n<=(s(#)Geo).n
proof
let pq,n;
consider x,y being object such that
A9: x in cT & y in cT and
A10: [x,y]=pq by ZFMISC_1:def 2;
reconsider x,y as Point of T by A9;
A11: (Geo.n)*s=(s(#)Geo).n by SEQ_1:9;
(1/2)|^n>0 by NEWTON:83;
then
A12: Geo.n>0 by PREPOWER:def 1;
consider pmet1 such that
A13: FS2.n=pmet1 and
A14: pmet1 is_a_pseudometric_of cT and
A15: for pq holds pmet1.pq<=s and
for pmet19 st pmet1=pmet19 holds pmet19 is continuous by A2;
A16: 0<=pmet1.(x,y) by A14,NAGATA_1:29;
A17: pmet1.pq=(FS2#pq).n by A13,SEQFUNC:def 10;
then (Geo.n)*(FS2#pq).n<=(Geo.n)*s by A15,A12,XREAL_1:64;
hence thesis by A10,A16,A12,A17,A11,SEQ_1:8;
end;
A18: for p,q holds pmet.(p,q)=0 implies p=q
proof
let p,q;
assume that
A19: pmet.(p,q)=0 and
A20: p<>q;
set Q={q};
A21: not p in Q by A20,TARSKI:def 1;
set pq=[p,q];
A22: Sum(Geo(#)(FS2#pq))=0 by A5,A19;
A23: for n holds 0<=(Geo(#)(FS2#pq)).n & (Geo(#)(FS2#pq)).n<=(s(#)Geo).n by A8;
Q is closed by A1,URYSOHN1:19;
then consider n such that
A24: for pmet1 st FS2.n=pmet1 holds lower_bound(pmet1,Q).p>0 by A3,A21;
consider pmet1 such that
A25: FS2.n=pmet1 and
A26: pmet1 is_a_pseudometric_of cT and
for pq holds pmet1.pq<=s and
for pmet19 st pmet1=pmet19 holds pmet19 is continuous by A2;
lower_bound(pmet1,Q).p> 0 by A24,A25;
then
A27: lower_bound(dist(pmet1,p).:Q)>0 by Def3;
(1/2)<1;
then |.1/2.|<1 by ABSVALUE:def 1;
then Geo is summable by SERIES_1:24;
then s(#)Geo is summable by SERIES_1:10;
then Geo(#)(FS2#pq) is summable by A23,SERIES_1:20;
then (Geo(#)(FS2#pq)).n=0 by A23,A22,RSSPACE:17;
then
A28: Geo.n *(FS2#pq).n=0 by SEQ_1:8;
(1/2)|^n>0 by NEWTON:83;
then Geo.n<>0 by PREPOWER:def 1;
then
A29: (FS2#pq).n=0 by A28,XCMPLX_1:6;
A30: pmet1.(p,q)=dist(pmet1,p).q by Def2;
dom dist(pmet1,p)=cT & q in Q by FUNCT_2:def 1,TARSKI:def 1;
then
A31: dist(pmet1,p).q in dist(pmet1,p).:Q by FUNCT_1:def 6;
dist(pmet1,p).:Q is non empty bounded_below by A26,Lm1;
then dist(pmet1,p).q>0 by A31,A27,SEQ_4:def 2;
hence thesis by A25,A29,A30,SEQFUNC:def 10;
end;
pmet is_a_pseudometric_of cT by A2,A5,Th15;
then pmet is Reflexive discerning symmetric triangle by A18,METRIC_1:def 3
,NAGATA_1:def 10;
then
A32: pmet is_metric_of cT by METRIC_6:3;
hence ex pmet st pmet is_metric_of the carrier of T & for pq holds pmet.pq=
Sum((1/2)GeoSeq(#)(FS2#pq)) by A5;
for A be non empty Subset of T holds Cl A
={p where p is Point of T:lower_bound(
pmet,A).p=0}
proof
let A be non empty Subset of T;
set INF={p where p is Point of T:lower_bound(pmet,A).p=0};
A33: INF c= Cl A
proof
let x be object;
assume x in INF;
then consider p be Point of T such that
A34: x=p and
A35: lower_bound(pmet,A).p=0;
A36: lower_bound(dist(pmet,p).:A)=0 by A35,Def3;
pmet is_a_pseudometric_of cT by A2,A5,Th15;
then
A37: dist(pmet,p).:A is non empty bounded_below by Lm1;
A38: A c= Cl A & ex y being object st y in A by PRE_TOPC:18,XBOOLE_0:def 1;
A39: A c= Cl A by PRE_TOPC:18;
assume not x in Cl A;
then consider n such that
A40: for pmet1 st FS2.n=pmet1 holds lower_bound(pmet1,Cl A).p>0 by A3,A34,A38;
(1/2)|^n>0 by NEWTON:83;
then
A41: Geo.n>0 by PREPOWER:def 1;
(1/2)|^n>0 by NEWTON:83;
then
A42: Geo.n>0 by PREPOWER:def 1;
consider pmet1 such that
A43: FS2.n=pmet1 and
A44: pmet1 is_a_pseudometric_of cT and
for pq holds pmet1.pq<=s and
for pmet19 st pmet1=pmet19 holds pmet19 is continuous by A2;
set r=Geo.n*lower_bound(pmet1,Cl A).p;
A45: lower_bound(dist(pmet1,p).:(Cl A))= lower_bound(pmet1,Cl A).p by Def3;
A46: lower_bound(pmet1,Cl A).p>0 by A40,A43;
then r>0 by A41,XREAL_1:129;
then r/2>0 by XREAL_1:215;
then consider rn such that
A47: rn in dist(pmet,p).:A and
A48: rn<lower_bound(dist(pmet,p).:A)+r/2 by A37,SEQ_4:def 2;
consider a be object such that
A49: a in dom dist(pmet,p) and
A50: a in A and
A51: rn=dist(pmet,p).a by A47,FUNCT_1:def 6;
reconsider a as Point of T by A49;
reconsider pa=[p,a] as Element of [:cT,cT:];
A52: dist(pmet1,p).a=pmet1.(p,a) by Def2;
dom dist(pmet1,p)=cT by FUNCT_2:def 1;
then
A53: dist(pmet1,p).a in dist(pmet1,p).:(Cl A) by A50,A39,FUNCT_1:def 6;
dist(pmet1,p).:(Cl A) is non empty bounded_below by A44,A50,A39,Lm1;
then lower_bound(pmet1,Cl A).p<=dist(pmet1,p).a by A53,A45,SEQ_4:def 2;
then lower_bound(pmet1,Cl A).p<=(FS2#pa).n by A43,A52,SEQFUNC:def 10;
then r<=Geo.n *(FS2#pa).n by A42,XREAL_1:64;
then
A54: r<=(Geo(#)(FS2#pa)).n by SEQ_1:8;
A55: for k holds 0<=(Geo(#)(FS2#pa)).k & (Geo(#)(FS2#pa)).k<=(s(#)Geo).k
by A8;
pmet.pa=pmet.(p,a);
then
A56: rn=pmet.pa by A51,Def2;
1/2<1;
then |.1/2.|<1 by ABSVALUE:def 1;
then Geo is summable by SERIES_1:24;
then s(#)Geo is summable by SERIES_1:10;
then Geo(#)(FS2#pa) is summable by A55,SERIES_1:20;
then (Geo(#)(FS2#pa)).n <=Sum(Geo(#)(FS2#pa)) by A55,RSSPACE2:3;
then rn>=(Geo(#)(FS2#pa)).n by A5,A56;
then (Geo(#)(FS2#pa)).n <r/2 by A48,A36,XXREAL_0:2;
then r<r/2 by A54,XXREAL_0:2;
hence thesis by A41,A46,XREAL_1:129,216;
end;
Cl A c= INF
proof
let x be object;
assume
A57: x in Cl A;
then reconsider p=x as Point of T;
pmet is_a_pseudometric_of cT & for pmet9 st pmet=pmet9 holds pmet9
is continuous by A2,A5,Th15;
then lower_bound(pmet,A).p=0 by A57,Th16;
hence thesis;
end;
hence thesis by A33;
end;
hence thesis by A32,Th10;
end;
theorem Th18:
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)
proof
let D be non empty set, p,q be FinSequence of D,B be BinOp of D such that
A1: p is one-to-one and
A2: q is one-to-one and
A3: rng q c= rng p and
A4: B is commutative associative and
A5: B is having_a_unity or len q>=1 & len p>len q;
A6: card (rng p)=len p by A1,FINSEQ_4:62;
consider r be FinSequence such that
A7: rng r=rng p \rng q and
A8: r is one-to-one by FINSEQ_4:58;
reconsider r as FinSequence of D by A7,FINSEQ_1:def 4;
rng (q^r)=rng q \/(rng p\ rng q ) by A7,FINSEQ_1:31;
then
A9: rng (q^r)=rng p by A3,XBOOLE_1:45;
rng r misses rng q by A7,XBOOLE_1:79;
then
A10: q^r is one-to-one by A2,A8,FINSEQ_3:91;
then card (rng (q^r))=len (q^r) by FINSEQ_4:62;
then len q < len q+ len r or B is having_a_unity by A5,A9,A6,FINSEQ_1:22;
then
A11: 1<=len r& 1<=len q & 1<=len p or B is having_a_unity by A5,NAT_1:19
,XXREAL_0:2;
ex P be Permutation of dom p st p*P=(q^r) & dom P = dom p & rng P = dom
p by A1,A10,A9,BHSP_5:1;
then
A12: B "**" p= B "**" (q^r) by A4,A11,FINSOP_1:7;
B "**" (q ^ r) = B.(B "**" q,B "**" r) by A4,A11,FINSOP_1:5;
hence thesis by A7,A8,A12;
end;
Lm2: PairFunc" = PairFunc qua Function" by Th2,TOPS_2:def 4;
reconsider jj=1 as Real;
::$N Nagata-Smirnov metrization theorem
theorem Th19:
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
proof
let T;
thus (T is regular & T is T_1 & ex Bn being FamilySequence of T st Bn is
Basis_sigma_locally_finite) implies T is metrizable
proof
set cTT=the carrier of [:T,T:];
set bcT = bool the carrier of T;
set cT = the carrier of T;
assume that
A1: T is regular and
A2: T is T_1 and
A3: ex Bn be FamilySequence of T st Bn is Basis_sigma_locally_finite;
set Fun=Funcs(cTT,REAL);
consider Bn be FamilySequence of T such that
A4: Bn is Basis_sigma_locally_finite by A3;
defpred NN[object,object,RealMap of [:T,T:]] means
ex pmet st $3=pmet & $3 is
continuous & pmet is_a_pseudometric_of cT & for p,q holds pmet.[p,q]<=1 & for p
,q st ex A,B st A is open & B is open & A in Bn.$2 & B in Bn.$1 & p in A & Cl A
c= B & not q in B holds pmet.[p,q] =1;
defpred N[object,object] means
ex F be RealMap of [:T,T:] st F = $2 & for n,m st
PairFunc".$1=[n,m] holds NN[n,m,F];
A5: Union Bn is Basis of T by A4,NAGATA_1:def 6;
A6: Bn is sigma_locally_finite by A4,NAGATA_1:def 6;
A7: for n,m ex pmet9 st NN[n,m,pmet9]
proof
defpred add9[Element of Fun,Element of Fun,set] means $1+$2=$3;
defpred funcdist[RealMap of T,Function] means for p,q holds $2.(p,q)=
|.$1.p-$1.q.|;
let n,m;
deffunc V(object)=
union{Q where Q is Subset of T:
ex D1 being set st D1 = $1 & Q in Bn.m & Cl Q c= D1};
set Bnn = Bn.n;
deffunc s(Subset of T)={Q where Q is Subset of T: Q in Bn.n& Q meets $1};
defpred S[set,Subset of T] means $1 in $2 & $2 is open & s($2) is finite;
A8: for A be object st A in bcT holds V(A) in bcT
proof
let A be object such that
A in bcT;
set Um={Q where Q is Subset of T:
ex D1 being set st D1 = A & Q in Bn.m & Cl Q c=D1};
now
let uv be object;
assume uv in V(A);
then consider v be set such that
A9: uv in v and
A10: v in Um by TARSKI:def 4;
ex B st v=B & ex D1 being set st D1 = A & B in Bn.m & Cl B c=D1
by A10;
hence uv in cT by A9;
end;
then V(A) c= cT;
hence thesis;
end;
consider Vm be Function of bcT,bcT such that
A11: for A be object st A in bcT holds Vm.A=V(A) from FUNCT_2:sch 2(A8
);
defpred F[object,object] means
ex F be RealMap of T, S be Subset of T st S =
$1 & F = $2 & F is continuous & (for p holds 0 <= F.p & F.p <= 1 & (p in S`
implies F.p = 0) & (p in Cl (Vm.S) implies F.p = 1));
A12: m in NAT by ORDINAL1:def 12;
A13: Bn.m is locally_finite by A6,NAGATA_1:def 3,A12;
A14: for A holds Cl (Vm.A) c=A
proof
let A;
set VmA={Q where Q is Subset of T:
ex D1 being set st D1 = A & Q in Bn.m & Cl Q c=D1};
VmA c= bcT
proof
let B be object;
assume B in VmA;
then ex C st B=C &
ex D1 being set st D1 = A & C in Bn.m & Cl C c=D1;
hence thesis;
end;
then reconsider VmA as Subset-Family of T;
A15: union clf VmA c= A
proof
let ClBu be object;
assume ClBu in union clf VmA;
then consider ClB be set such that
A16: ClBu in ClB and
A17: ClB in clf VmA by TARSKI:def 4;
reconsider ClB as Subset of T by A17;
consider B such that
A18: Cl B =ClB and
A19: B in VmA by A17,PCOMPS_1:def 2;
ex C st B=C &
ex D1 being set st D1 = A & C in Bn.m & Cl C c=D1 by A19;
hence thesis by A16,A18;
end;
VmA c=Bn.m
proof
let B be object;
assume B in VmA;
then ex C st B=C &
ex D1 being set st D1 = A & C in Bn.m & Cl C c=D1;
hence thesis;
end;
then
A20: Cl union VmA = union clf VmA by A13,PCOMPS_1:9,20;
Vm.A=V(A) by A11;
hence Cl (Vm.A) c=A by A15,A20;
end;
A21: for A be object st A in Bnn
ex f be object st f in Funcs(cT,REAL) & F[A,f ]
proof
let A be object;
assume A in Bnn;
then
A22: A in Union Bn by PROB_1:12;
Union Bn c= the topology of T by A5,TOPS_2:64;
then reconsider A as open Subset of T by A22,PRE_TOPC:def 2;
A` misses A by XBOOLE_1:79;
then
A23: A` misses Cl (Vm.A) by A14,XBOOLE_1:63;
T is normal by A1,A4,NAGATA_1:20;
then consider f be Function of T,R^1 such that
A24: f is continuous & for p holds 0 <= f.p & f.p <= 1 & (p in A`
implies f.p=0)& (p in Cl (Vm.A) implies f.p=1) by A23,URYSOHN3:20;
reconsider f9=f as RealMap of T by TOPMETR:17;
A25: ex F be RealMap of T, S be Subset of T st S = A & F = f9 & F is
continuous & for p holds 0 <= F.p & F.p <= 1 & (p in S` implies F.p = 0) & (p
in Cl (Vm.S) implies F.p = 1)
proof
take f9, A;
thus thesis by A24,JORDAN5A:27;
end;
f9 in Funcs(cT,REAL) by FUNCT_2:8;
hence thesis by A25;
end;
consider Fn be Function of Bnn,Funcs(cT,REAL) such that
A26: for A be object st A in Bnn holds F[A,Fn.A] from FUNCT_2:sch 1(A21
);
A27: n in NAT by ORDINAL1:def 12;
Bn.n is locally_finite by A6,NAGATA_1:def 3,A27;
then
A28: for p being Element of cT ex A be Element of bcT st S[p,A] by
PCOMPS_1:def 1;
consider Sx be Function of cT,bcT such that
A29: for p be Element of cT holds S[p,Sx.p] from FUNCT_2:sch 3(A28);
defpred ss[object,object] means
for x,y be Element of T st $1=[x,y] holds $2=
[:Sx.x,Sx.y:];
A30: for pq9 be object st pq9 in cTT
ex SS be object st SS in bool cTT & ss[ pq9,SS]
proof
let pq9 be object;
assume pq9 in cTT;
then pq9 in [:cT,cT:] by BORSUK_1:def 2;
then consider p,q be object such that
A31: p in cT & q in cT and
A32: pq9=[p,q] by ZFMISC_1:def 2;
reconsider p,q as Point of T by A31;
now
let p1,q1 be Point of T;
assume
A33: pq9=[p1,q1];
then p1=p by A32,XTUPLE_0:1;
hence [:Sx.p,Sx.q:]=[:Sx.p1,Sx.q1:] by A32,A33,XTUPLE_0:1;
end;
hence thesis;
end;
consider SS be Function of cTT,bool cTT such that
A34: for pq be object st pq in cTT holds ss[pq,SS.pq] from FUNCT_2:sch
1(A30);
A35: for pq9 holds pq9 in SS.pq9 & SS.pq9 is open
proof
let pq9 be Point of [:T,T:];
pq9 in cTT;
then pq9 in [:cT,cT:] by BORSUK_1:def 2;
then consider p,q be object such that
A36: p in cT & q in cT and
A37: pq9=[p,q] by ZFMISC_1:def 2;
reconsider p,q as Point of T by A36;
A38: p in Sx.p & q in Sx.q by A29;
A39: Sx.p is open & Sx.q is open by A29;
SS.pq9=[:Sx.p,Sx.q:] by A34,A37;
hence thesis by A37,A38,A39,BORSUK_1:6,ZFMISC_1:def 2;
end;
A40: for f,g be Element of Fun ex fg be Element of Fun st add9[f,g,fg]
proof
let f,g be Element of Fun;
set f9=f,g9=g;
f9+g9 in Fun by FUNCT_2:8;
hence thesis;
end;
consider ADD be BinOp of Funcs(the carrier of [:T,T:],REAL) such that
A41: for f,g be Element of Fun holds add9[f,g,ADD.(f,g)] from
BINOP_1:sch 3(A40);
A42: for f be Element of Funcs(cT,REAL) ex fxy be Element of Fun st
funcdist[f,fxy]
proof
let f be Element of Funcs(cT,REAL);
defpred fd[Element of T,Element of T,object] means $3=|.f.$1-f.$2.|;
A43: for x,y be Element of cT ex r be Element of REAL st fd[x,y,r]
proof let x,y be Element of cT;
consider r be Real such that
A44: fd[x,y,r];
reconsider r as Element of REAL by XREAL_0:def 1;
fd[x,y,r] by A44;
hence thesis;
end;
consider Fd be Function of [:cT,cT:],REAL such that
A45: for x,y be Element of cT holds fd[x,y,Fd.(x,y)] from BINOP_1:
sch 3(A43);
[:cT,cT:]= cTT by BORSUK_1:def 2;
then Fd in Fun by FUNCT_2:8;
hence thesis by A45;
end;
consider Fdist be Function of Funcs(cT,REAL),Fun such that
A46: for fd be Element of Funcs(cT,REAL) holds funcdist[fd,Fdist.fd]
from FUNCT_2:sch 3(A42);
deffunc Fx(Element of T)= {Fn.A where A is Subset of T:A in Bn.n & A in
s(Sx.$1)};
deffunc RNG(set)={Fdist.fd where fd is RealMap of T:fd in $1};
defpred gxy[set,Function] means $2 is one-to-one & ex p,q st [p,q]=$1 &
rng $2=RNG(Fx(p)\/Fx(q));
A47: for p holds Fx(p) is finite
proof
deffunc Fxx(Subset of T)=Fn.$1;
let p;
set SFxx={Fxx(A) where A is Subset of T:A in s(Sx.p)};
A48: Fx(p) c= SFxx
proof
let FA be object;
assume FA in Fx(p);
then ex A st FA=Fn.A & A in Bn.n & A in s(Sx.p);
hence thesis;
end;
A49: s(Sx.p) is finite by A29;
SFxx is finite from FRAENKEL:sch 21(A49);
hence thesis by A48;
end;
A50: for p,q holds RNG(Fx(p)\/Fx(q)) is finite & RNG(Fx(p)\/Fx(q))c=Fun
proof
deffunc FD(RealMap of T)=Fdist.$1;
let p,q;
A51: RNG(Fx(p)\/Fx(q)) c=Fun
proof
let FDm be object;
assume FDm in RNG(Fx(p)\/Fx(q));
then consider fd be RealMap of T such that
A52: FDm=Fdist.fd and
fd in Fx(p)\/Fx(q);
fd in Funcs(cT,REAL) by FUNCT_2:8;
hence thesis by A52,FUNCT_2:5;
end;
set RNG9={FD(fd) where fd is Element of Funcs(cT,REAL): fd in Fx(p)\/
Fx(q)};
A53: RNG(Fx(p)\/Fx(q))c=RNG9
proof
let Fdistfd be object;
assume Fdistfd in RNG(Fx(p)\/Fx(q));
then consider fd be RealMap of T such that
A54: Fdistfd =Fdist.fd & fd in Fx(p)\/Fx(q);
fd in Funcs(cT,REAL) by FUNCT_2:8;
hence thesis by A54;
end;
Fx(p) is finite & Fx(q) is finite by A47;
then
A55: Fx(p)\/Fx(q) is finite;
RNG9 is finite from FRAENKEL:sch 21(A55);
hence thesis by A51,A53;
end;
A56: for pq be Element of cTT ex G be Element of Fun* st gxy[pq,G]
proof
let pq be Element of cTT;
pq in the carrier of [:T,T:];
then pq in [:cT,cT:] by BORSUK_1:def 2;
then consider p,q be object such that
A57: p in cT & q in cT and
A58: pq=[p,q] by ZFMISC_1:def 2;
reconsider p,q as Point of T by A57;
consider SF be FinSequence such that
A59: rng SF =RNG(Fx(p)\/Fx(q)) and
A60: SF is one-to-one by A50,FINSEQ_4:58;
rng SF c=Fun by A50,A59;
then reconsider SF as FinSequence of Fun by FINSEQ_1:def 4;
SF in Fun* by FINSEQ_1:def 11;
hence thesis by A58,A59,A60;
end;
consider SFdist be Function of cTT,Fun* such that
A61: for pq be Element of cTT holds gxy[pq,SFdist.pq] from FUNCT_2:
sch 3(A56);
defpred SFdist[object,object] means
for FS be FinSequence of Fun st FS=SFdist.
$1 holds $2= ADD "**" FS;
A62: for pq be object st pq in cTT
ex S be object st S in Fun & SFdist[pq,S]
proof
let pq be object;
assume pq in cTT;
then SFdist.pq in Fun* by FUNCT_2:5;
then reconsider SF=SFdist.pq as FinSequence of Fun by FINSEQ_1:def 11;
for FS be FinSequence of Funcs(cTT,REAL) st FS=SFdist.pq holds
ADD "**" FS = ADD "**" SF;
hence thesis;
end;
consider SumFdist be Function of cTT,Funcs(cTT,REAL) such that
A63: for xy be object st xy in cTT holds SFdist[xy,SumFdist.xy] from
FUNCT_2:sch 1(A62);
reconsider SumFdist9=SumFdist as Function of cTT,Funcs(cTT,the carrier
of R^1) by TOPMETR:17;
reconsider SumFTS9=SumFdist9 Toler as RealMap of [:T,T:] by TOPMETR:17;
cTT=[:cT,cT:] by BORSUK_1:def 2;
then reconsider
SumFTS = SumFdist9 Toler as Function of [:cT,cT:],REAL by TOPMETR:17;
A64: for f1,f2 be RealMap of [:T,T:] holds ADD.(f1,f2)=f1+f2
proof
let f1,f2 be RealMap of [:T,T:];
reconsider f19=f1,f29=f2 as Element of Fun by FUNCT_2:8;
ADD.(f19,f29)=f19+f29 by A41;
hence thesis;
end;
A65: for p,q st ex A,B st A is open & B is open & A in Bn.m & B in Bn.n
& p in A & Cl A c= B & not q in B holds SumFTS9.[p,q] >= 1
proof
let p,q;
assume ex A,B st A is open & B is open & A in Bn.m & B in Bn.n & p
in A & Cl A c= B & not q in B;
then consider A,B such that
A is open and
B is open and
A66: A in Bn.m and
A67: B in Bn.n and
A68: p in A and
A69: Cl A c= B and
A70: not q in B;
A71: F[B,Fn.B] by A26,A67;
A in {Q where Q is Subset of T:
ex D1 being set st D1 = B & Q in Bn.m & Cl Q c=D1} by A66,A69;
then A c=V(B) by ZFMISC_1:74;
then
A72: A c= Vm.B by A11;
Vm.B c= Cl(Vm.B) by PRE_TOPC:18;
then
A73: p in Cl(Vm.B) by A68,A72;
Cl(Vm.B)c=B & p in Sx.p by A14,A29;
then Sx.p meets B by A73,XBOOLE_0:3;
then
A74: B in s(Sx.p) by A67;
reconsider pq=[p,q] as Point of [:T,T:] by BORSUK_1:def 2;
reconsider SF=SFdist.pq as FinSequence of Fun by FINSEQ_1:def 11;
consider x,y be Point of T such that
A75: [x,y]=pq and
A76: rng SF=RNG(Fx(x)\/Fx(y)) by A61;
reconsider ASF=ADD"**"SF as RealMap of [:T,T:] by FUNCT_2:66;
assume
A77: SumFTS9.[p,q] < 1;
reconsider FnB=Fn.B as RealMap of T by A67,FUNCT_2:5,66;
A78: FnB in Funcs(cT,REAL) by A67,FUNCT_2:5;
q in B` by A70,XBOOLE_0:def 5;
then
A79: FnB.q=0 by A71;
x=p by A75,XTUPLE_0:1;
then FnB in Fx(x) by A67,A74;
then FnB in Fx(x)\/Fx(y) by XBOOLE_0:def 3;
then
A80: Fdist.FnB in rng SF by A76;
then reconsider FdistFnB=Fdist.FnB as RealMap of [:T,T:] by FUNCT_2:66;
SF<>{} by A80,RELAT_1:38;
then len SF >=1 by NAT_1:14;
then consider F be sequence of Fun such that
A81: F.1 = SF.1 and
A82: for n being Nat st 0 <> n & n < len SF holds F.(n+1)=ADD.(F.n,SF.(n+1))
and
A83: ADD"**"SF=F.(len SF) by FINSOP_1:def 1;
A84: SumFTS.pq=SumFdist.pq.pq & SumFdist.pq=ASF by A63,NAGATA_1:def 8;
defpred P[Nat] means
for k st k<>0 & k<=$1 & $1<=len SF for
fk,Fn be RealMap of [:T,T:] st fk=SF.k & Fn=F.$1 holds fk.pq<=Fn.pq;
A85: for k st k <>0 & k <=len SF for f be RealMap of [:T,T:] st f=SF.
k holds f.pq>=0
proof
let k such that
A86: k <>0 and
A87: k <=len SF;
k >=1 by A86,NAT_1:14;
then k in dom SF by A87,FINSEQ_3:25;
then SF.k in RNG(Fx(x)\/Fx(y)) by A76,FUNCT_1:def 3;
then consider fd be RealMap of T such that
A88: Fdist.fd =SF.k and
fd in Fx(x)\/Fx(y);
let f be RealMap of [:T,T:] such that
A89: f=SF.k;
fd in Funcs(cT,REAL) by FUNCT_2:8;
then f.(p,q)=|.fd.p-fd.q.| by A46,A89,A88;
hence thesis by COMPLEX1:46;
end;
A90: for i holds P[i] implies P[i+1]
proof
let i;
assume
A91: P[i];
let k such that
A92: k<>0 and
A93: k<=i+1 and
A94: i+1<=len SF;
now
1<=i+1 by NAT_1:14;
then i+1 in dom SF by A94,FINSEQ_3:25;
then SF.(i+1) in rng SF by FUNCT_1:def 3;
then reconsider SFi1=SF.(i+1) as RealMap of [:T,T:] by FUNCT_2:66;
reconsider Fi=F.i as RealMap of [:T,T:] by FUNCT_2:66;
let fk,Fn be RealMap of [:T,T:] such that
A95: fk=SF.k and
A96: Fn=F.(i+1);
per cases by A93,XXREAL_0:1;
suppose
A97: k<i+1;
A98: i<len SF by A94,NAT_1:13;
i<>0 by A92,A97,NAT_1:13;
then F.(i+1)=ADD.(F.i,SF.(i+1)) by A82,A98;
then
A99: Fn =Fi+SFi1 by A64,A96;
SFi1.pq>=0 by A85,A94;
then Fi.pq +0 <= Fi.pq + SFi1.pq by XREAL_1:7;
then
A100: Fn.pq>=Fi.pq by A99,NAGATA_1:def 7;
A101: i<=len SF by A94,NAT_1:13;
k<=i by A97,NAT_1:13;
then fk.pq<=Fi.pq by A91,A92,A95,A101;
hence fk.pq<=Fn.pq by A100,XXREAL_0:2;
end;
suppose
A102: k=i+1;
per cases;
suppose
i=0;
hence fk.pq<=Fn.pq by A81,A95,A96,A102;
end;
suppose
A103: i<>0;
i+0<i+1 by XREAL_1:8;
then
A104: i<len SF by A94,XXREAL_0:2;
1<=i by A103,NAT_1:14;
then i in dom SF by A104,FINSEQ_3:25;
then SF.i in rng SF by FUNCT_1:def 3;
then reconsider SFi=SF.i as RealMap of [:T,T:] by FUNCT_2:66;
0<=SFi.pq by A85,A103,A104;
then 0<=Fi.pq by A91,A103,A104;
then
A105: Fi.pq+fk.pq>=0+fk.pq by XREAL_1:7;
F.(i+1)=ADD.(F.i,SF.(i+1)) by A82,A103,A104;
then Fn=Fi+fk by A64,A95,A96,A102;
hence fk.pq<=Fn.pq by A105,NAGATA_1:def 7;
end;
end;
end;
hence thesis;
end;
A106: P[ 0 ];
A107: for i holds P[i] from NAT_1:sch 2(A106,A90);
consider k be object such that
A108: k in dom SF and
A109: SF.k=Fdist.FnB by A80,FUNCT_1:def 3;
A110: k in Seg(len SF) by A108,FINSEQ_1:def 3;
FnB.p =1 by A73,A71;
then
A111: FdistFnB.(p,q)=|.1-0 .| by A46,A78,A79;
reconsider k as Element of NAT by A108;
A112: |.1.|=1 by ABSVALUE:def 1;
k<>0 & k <=len SF by A110,FINSEQ_1:1;
hence thesis by A77,A84,A83,A107,A111,A112,A109;
end;
A113: now
let p,q;
assume ex A,B st A is open & B is open & A in Bn.m & B in Bn.n & p
in A & Cl A c= B & not q in B;
then SumFTS9.[p,q]>=1 by A65;
then
A114: 1 = min(1,SumFTS9.[p,q]) by XXREAL_0:def 9;
[:cT,cT:]=cTT by BORSUK_1:def 2;
hence 1=min(jj,SumFTS9).[p,q] by A114,NAGATA_1:def 9;
end;
A115: for pq be Element of cTT, map9 be Element of Fun st map9
is_a_unity_wrt ADD holds map9.pq=0
proof
let pq be Element of cTT, map9 be Element of Fun;
assume map9 is_a_unity_wrt ADD;
then ADD.(map9,map9)=map9 by BINOP_1:3;
then (map9+map9).pq=map9.pq by A41;
then map9.pq+map9.pq=map9.pq by NAGATA_1:def 7;
hence thesis;
end;
A116: for pq1,pq2 be Point of [:T,T:] holds (pq1 in SS.pq2 implies
SumFdist.pq1.pq1 = SumFdist.pq2.pq1) & for SumFdist1,SumFdist2 be RealMap of [:
T,T:] st SumFdist1=SumFdist.pq1 & SumFdist2 = SumFdist.pq2 holds SumFdist1.pq1
>= SumFdist2.pq1
proof
deffunc No0(Element of T,Element of T)= {Fn.A where A is Subset of T:A
in Bn.n & for FnA be RealMap of T st Fn.A=FnA holds (FnA.$1 > 0 or FnA.$2 > 0)}
;
let pq1,pq2 be Point of [:T,T:];
reconsider S1=SFdist.pq1,S2=SFdist.pq2 as FinSequence of Fun by
FINSEQ_1:def 11;
consider p1,q1 be Point of T such that
A117: [p1,q1]=pq1 and
A118: rng S1=RNG(Fx(p1)\/Fx(q1)) by A61;
A119: for p,q,p1,q1 be Point of T st [p,q] in SS.[p1,q1] holds No0(p,q
) c= Fx(p1)\/Fx(q1)
proof
let p,q,p1,q1 be Point of T such that
A120: [p,q] in SS.[p1,q1];
reconsider pq1=[p1,q1] as Element of cTT by BORSUK_1:def 2;
[:Sx.p1,Sx.q1:]=SS.pq1 by A34;
then
A121: p in Sx.p1 & q in Sx.q1 by A120,ZFMISC_1:87;
let no0 be object;
assume no0 in No0(p,q);
then consider A be Subset of T such that
A122: no0=Fn.A and
A123: A in Bn.n and
A124: for FnA be RealMap of T st Fn.A=FnA holds (FnA.p > 0 or FnA.q > 0);
reconsider FnA=Fn.A as RealMap of T by A123,FUNCT_2:5,66;
A125: FnA.p > 0 or FnA.q > 0 by A124;
F[A,Fn.A] by A26,A123;
then not p in cT\A or not q in cT\A by A125;
then p in A or q in A by XBOOLE_0:def 5;
then A meets Sx.p1 or A meets Sx.q1 by A121,XBOOLE_0:3;
then A in s(Sx.p1) or A in s(Sx.q1) by A123;
then FnA in Fx(p1) or FnA in Fx(q1) by A123;
hence thesis by A122,XBOOLE_0:def 3;
end;
A126: RNG(No0(p1,q1))c=RNG(Fx(p1)\/Fx(q1))
proof
p1 in Sx.p1 & q1 in Sx.q1 by A29;
then [p1,q1] in [:Sx.p1,Sx.q1:] by ZFMISC_1:87;
then [p1,q1] in SS.[p1,q1] by A34;
then
A127: No0(p1,q1)c= Fx(p1)\/Fx(q1) by A119;
let FD be object;
assume FD in RNG(No0(p1,q1));
then ex fd be RealMap of T st FD=Fdist.fd & fd in (No0(p1,q1) );
hence thesis by A127;
end;
A128: for f be FinSequence of Funcs(cTT,REAL),p,q,p1,q1 be Point of T
st rng f= RNG(Fx(p1)\/Fx(q1))\RNG(No0(p,q)) holds (ADD "**" f).[p,q]=0
proof
let f be FinSequence of Funcs(cTT,REAL),p,q,p1,q1 be Point of T such
that
A129: rng f= RNG(Fx(p1)\/Fx(q1))\RNG(No0(p,q));
reconsider pq=[p,q] as Element of cTT by BORSUK_1:def 2;
now
per cases;
suppose
A130: len f = 0;
A131: ADD is having_a_unity by A64,NAGATA_1:23;
then
A132: ex f be Element of Fun st f is_a_unity_wrt ADD by SETWISEO:def 2;
ADD "**" f=the_unity_wrt ADD by A130,A131,FINSOP_1:def 1;
then ADD"**"f is_a_unity_wrt ADD by A132,BINOP_1:def 8;
hence (ADD"**"f).pq=0 by A115;
end;
suppose
A133: len f<>0;
then len f >=1 by NAT_1:14;
then consider F be sequence of Fun such that
A134: F.1 = f.1 and
A135: for n being Nat st 0 <> n & n < len f
holds F.(n + 1) = ADD.(F.n,f.(n + 1)) and
A136: ADD"**"f = F.(len f) by FINSOP_1:def 1;
defpred R[Nat] means
$1<>0 & $1<=len f implies F.$1.pq=0;
A137: for k holds R[k] implies R[k+1]
proof
let k;
assume
A138: R[k];
assume that
k+1<>0 and
A139: k+1 <=len f;
A140: k< len f by A139,NAT_1:13;
k+1>=1 by NAT_1:14;
then k+1 in dom f by A139,FINSEQ_3:25;
then
A141: f.(k+1) in RNG(Fx(p1)\/Fx(q1))\RNG(No0(p,q)) by A129,
FUNCT_1:def 3;
then f.(k+1) in RNG(Fx(p1)\/Fx(q1));
then consider fd be RealMap of T such that
A142: Fdist.fd =f.(k+1) and
A143: fd in Fx(p1)\/Fx(q1);
fd in Funcs(cT,REAL) by FUNCT_2:8;
then reconsider
Fdistfd=Fdist.fd,Fk1=F.(k+1), Fk=F.k,fk1=f.(k+1) as
RealMap of [:T,T:] by A142,FUNCT_2:5,66;
fd in Funcs(cT,REAL) by FUNCT_2:8;
then
A144: Fdistfd.(p,q)=|.fd.p- fd.q.| by A46;
A145: not f.(k+1) in RNG(No0(p,q)) by A141,XBOOLE_0:def 5;
A146: fd.p=0 & fd.q=0
proof
assume
A147: fd.p<>0 or fd.q<>0;
per cases by A143,XBOOLE_0:def 3;
suppose
fd in Fx(p1);
then consider A be Subset of T such that
A148: fd=Fn.A and
A149: A in Bn.n and
A in s(Sx.p1);
A150: F[A,Fn.A] by A26,A149;
not fd in No0(p,q) by A145,A142;
then ex FnA be RealMap of T st Fn.A=FnA &( not FnA.p > 0)&
not FnA.q > 0 by A148,A149;
hence contradiction by A147,A148,A150;
end;
suppose
fd in Fx(q1);
then consider A be Subset of T such that
A151: fd=Fn.A and
A152: A in Bn.n and
A in s(Sx.q1);
A153: F[A,Fn.A] by A26,A152;
not fd in No0(p,q) by A145,A142;
then ex FnA be RealMap of T st Fn.A=FnA &( not FnA.p > 0)&
not FnA.q > 0 by A151,A152;
hence contradiction by A147,A151,A153;
end;
end;
per cases;
suppose
k=0;
hence thesis by A134,A142,A146,A144,ABSVALUE:2;
end;
suppose
A154: k>0;
then Fk1=ADD.(Fk,fk1) by A135,A140;
then Fk1=Fk+fk1 by A64;
then Fk1.pq=0+fk1.pq by A138,A139,A154,NAGATA_1:def 7
,NAT_1:13;
hence thesis by A142,A146,A144,ABSVALUE:2;
end;
end;
A155: R[ 0 ];
for n holds R[n] from NAT_1:sch 2(A155,A137);
hence (ADD"**"f).pq=0 by A133,A136;
end;
end;
hence thesis;
end;
A156: RNG(Fx(p1)\/Fx(q1)) is finite by A50;
then consider No be FinSequence such that
A157: rng No =RNG(No0(p1,q1)) and
A158: No is one-to-one by A126,FINSEQ_4:58;
RNG(Fx(p1)\/Fx(q1))c=Fun by A50;
then
A159: RNG(No0(p1,q1)) c= Fun by A126;
then reconsider No as FinSequence of Fun by A157,FINSEQ_1:def 4;
consider p2,q2 be Point of T such that
A160: [p2,q2]=pq2 and
A161: rng S2=RNG(Fx(p2)\/Fx(q2)) by A61;
reconsider S1=SFdist.pq1,S2=SFdist.pq2 as FinSequence of Fun by
FINSEQ_1:def 11;
set RNiS2=RNG(No0(p1,q1))/\RNG(Fx(p2)\/Fx(q2));
A162: S2 is one-to-one by A61;
A163: ADD is having_a_unity & ADD is commutative associative by A64,
NAGATA_1:23;
S1 is one-to-one by A61;
then consider S1No be FinSequence of Fun such that
S1No is one-to-one and
A164: rng S1No=rng S1 \rng No and
A165: ADD"**"S1 =ADD.(ADD"**"No,ADD"**"S1No) by A118,A126,A157,A158,A163,Th18
;
consider NoiS2 be FinSequence such that
A166: rng NoiS2 =RNiS2 and
A167: NoiS2 is one-to-one by A126,A156,FINSEQ_4:58;
RNiS2 c=RNG(No0(p1,q1)) by XBOOLE_1:17;
then RNiS2 c= Fun by A159;
then reconsider NoiS2 as FinSequence of Fun by A166,FINSEQ_1:def 4;
rng NoiS2 c= rng No by A157,A166,XBOOLE_1:17;
then consider NoNoiS2 be FinSequence of Fun such that
NoNoiS2 is one-to-one and
A168: rng NoNoiS2=rng No \rng NoiS2 and
A169: ADD"**"No=ADD.(ADD"**"NoiS2,ADD"**"NoNoiS2) by A158,A163,A167,Th18;
rng NoiS2 c= rng S2 by A161,A166,XBOOLE_1:17;
then consider S2No be FinSequence of Fun such that
S2No is one-to-one and
A170: rng S2No=rng S2 \rng NoiS2 and
A171: ADD"**"S2=ADD.(ADD"**"NoiS2,ADD"**"S2No) by A163,A167,A162,Th18;
reconsider ANoNoiS2=ADD"**"NoNoiS2,ANo=ADD"**"No,AS1No=ADD"**"S1No,
AS2No=ADD"**"S2No,ANoiS2=ADD"**"NoiS2,AS1=ADD"**"S1,AS2=ADD"**"S2 as RealMap of
[:T,T:] by FUNCT_2:66;
rng S2No= RNG(Fx(p2)\/Fx(q2))\RNG(No0(p1,q1)) by A161,A166,A170,
XBOOLE_1:47;
then
A172: AS2No.pq1=0 by A128,A117;
ANo=ANoiS2+ANoNoiS2 by A64,A169;
then
A173: ANo.pq1=ANoiS2.pq1+ANoNoiS2. pq1 by NAGATA_1:def 7;
AS1=ANo+AS1No by A64,A165;
then
A174: AS1.pq1=ANo.pq1+AS1No.pq1 by NAGATA_1:def 7;
AS2=ANoiS2+AS2No by A64,A171;
then
A175: AS2.pq1=ANoiS2.pq1+AS2No.pq1 by NAGATA_1:def 7;
A176: AS1No.pq1=0 by A128,A117,A118,A157,A164;
thus pq1 in SS.pq2 implies SumFdist.pq1.pq1 = SumFdist.pq2.pq1
proof
A177: ADD is having_a_unity by A64,NAGATA_1:23;
then
A178: ex f be Element of Fun st f is_a_unity_wrt ADD by SETWISEO:def 2;
assume
A179: pq1 in SS.pq2;
now
let FD be object;
assume FD in RNG (No0(p1,q1));
then
A180: ex fd be RealMap of T st FD=Fdist.fd & fd in (No0(p1,q1) );
No0(p1,q1) c= Fx(p2)\/Fx(q2) by A119,A117,A160,A179;
hence FD in RNG(Fx(p2)\/Fx(q2)) by A180;
end;
then RNG (No0(p1,q1)) c= RNG(Fx(p2)\/Fx(q2));
then RNiS2=RNG(No0(p1,q1)) by XBOOLE_1:28;
then rng NoNoiS2={} by A157,A166,A168,XBOOLE_1:37;
then NoNoiS2={} by RELAT_1:41;
then len NoNoiS2 =0;
then ADD"**"NoNoiS2=the_unity_wrt ADD by A177,FINSOP_1:def 1;
then ADD"**"NoNoiS2 is_a_unity_wrt ADD by A178,BINOP_1:def 8;
then
A181: AS1.pq1=AS2.pq1 by A115,A174,A173,A175,A176,A172;
SumFdist.pq1=AS1 by A63;
hence thesis by A63,A181;
end;
A182: ANoNoiS2.(p1,q1)>=0
proof
set N=NoNoiS2;
per cases;
suppose
A183: len N=0;
A184: ADD is having_a_unity by A64,NAGATA_1:23;
then
A185: ex f be Element of Fun st f is_a_unity_wrt ADD by SETWISEO:def 2;
ADD "**" N=the_unity_wrt ADD by A183,A184,FINSOP_1:def 1;
then ADD"**"N is_a_unity_wrt ADD by A185,BINOP_1:def 8;
hence thesis by A115,A117;
end;
suppose
A186: len N<>0;
then len N >=1 by NAT_1:14;
then consider F be sequence of Fun such that
A187: F.1 = N.1 and
A188: for n being Nat st 0 <> n & n < len N
holds F.(n + 1) = ADD.(F.n,N.(n + 1)) and
A189: ADD "**" N=F.(len N) by FINSOP_1:def 1;
defpred R[Nat] means
$1<>0 & $1<=len N implies for Fn
be RealMap of [:T,T:] st Fn=F.$1 holds Fn.(p1,q1)>=0;
A190: for k holds R[k] implies R[k+1]
proof
let k;
assume
A191: R[k];
assume that
k+1<>0 and
A192: k+1 <=len N;
A193: k< len N by A192,NAT_1:13;
k+1>=1 by NAT_1:14;
then k+1 in dom N by A192,FINSEQ_3:25;
then N.(k+1) in rng No \rng NoiS2 by A168,FUNCT_1:def 3;
then N.(k+1) in RNG(No0(p1,q1)) by A157,XBOOLE_0:def 5;
then consider fd be RealMap of T such that
A194: Fdist.fd =N.(k+1) and
fd in No0(p1,q1);
fd in Funcs(cT,REAL) by FUNCT_2:8;
then reconsider
Fdistfd=Fdist.fd,Fk1=F.(k+1), Fk=F.k,Nk1=N.(k+1) as
RealMap of [:T,T:] by A194,FUNCT_2:5,66;
A195: |.fd.p1-fd.q1.|>=0 by COMPLEX1:46;
A196: fd in Funcs(cT,REAL) by FUNCT_2:8;
then
A197: Fdistfd.(p1,q1)=|.fd. p1-fd.q1.| by A46;
A198: now
per cases;
suppose
k=0;
hence Fk1.(p1,q1)>=0 by A46,A187,A194,A196,A195;
end;
suppose
A199: k>0;
Fk1=ADD.(Fk,Nk1) by A188,A193,A199;
then
A200: Fk1=Fk+Nk1 by A64;
Fk.(p1,q1) >= 0 by A191,A192,A199,NAT_1:13;
then 0+0<=Fk.(p1,q1)+Nk1.(p1,q1) by A194,A195,A197;
hence Fk1.(p1,q1) >=0 by A117,A200,NAGATA_1:def 7;
end;
end;
let Fn be RealMap of [:T,T:];
assume Fn=F.(k+1);
hence thesis by A198;
end;
A201: R[ 0 ];
for n holds R[n] from NAT_1:sch 2(A201,A190);
hence thesis by A186,A189;
end;
end;
now
A202: AS2.(p1,q1)<=AS1.(p1,q1) by A117,A182,A174,A173,A175,A176,A172,
XREAL_1:7;
let SumFdist1,SumFdist2 be RealMap of [:T,T:];
assume that
A203: SumFdist1=SumFdist.pq1 and
A204: SumFdist2 = SumFdist.pq2;
SumFdist2=AS2 by A63,A204;
hence SumFdist1.pq1 >= SumFdist2.pq1 by A63,A117,A203,A202;
end;
hence thesis;
end;
now
let p,q,r be Point of T;
thus SumFTS.(p,p)=0
proof
reconsider pp=[p,p] as Point of [:T,T:] by BORSUK_1:def 2;
reconsider SF=SFdist.pp as FinSequence of Fun by FINSEQ_1:def 11;
A205: now
per cases;
suppose
A206: len SF=0;
A207: ADD is having_a_unity by A64,NAGATA_1:23;
then
A208: ex f be Element of Fun st f is_a_unity_wrt ADD by SETWISEO:def 2;
ADD "**" SF=the_unity_wrt ADD by A206,A207,FINSOP_1:def 1;
then ADD"**"SF is_a_unity_wrt ADD by A208,BINOP_1:def 8;
hence (ADD"**"SF).pp=0 by A115;
end;
suppose
A209: len SF <>0;
then len SF >=1 by NAT_1:14;
then consider F be sequence of Fun such that
A210: F.1 = SF.1 and
A211: for n being Nat
st 0 <> n & n < len SF holds F.(n + 1) = ADD.(F.
n,SF.(n + 1 )) and
A212: ADD"**"SF = F.(len SF) by FINSOP_1:def 1;
defpred R[Nat] means
$1<>0 & $1<=len SF implies F.$1.pp=0;
A213: for k holds R[k] implies R[k+1]
proof
let k;
assume
A214: R[k];
consider x,y be Point of T such that
[x,y]=pp and
A215: rng SF=RNG(Fx(x)\/Fx(y)) by A61;
assume that
k+1<>0 and
A216: k+1 <=len SF;
A217: k< len SF by A216,NAT_1:13;
k+1>=1 by NAT_1:14;
then k+1 in dom SF by A216,FINSEQ_3:25;
then SF.(k+1) in RNG(Fx(x)\/Fx(y)) by A215,FUNCT_1:def 3;
then consider fd be RealMap of T such that
A218: Fdist.fd =SF.(k+1) and
fd in Fx(x)\/Fx(y);
fd in Funcs(cT,REAL) by FUNCT_2:8;
then reconsider
Fdistfd=Fdist.fd,Fk1=F.(k+1),Fk=F.k, SFk1=SF.(k+1)
as RealMap of [:T,T:] by A218,FUNCT_2:5,66;
fd in Funcs(cT,REAL) by FUNCT_2:8;
then
A219: Fdistfd.(p,p)=|.fd.p-fd .p.| by A46;
per cases;
suppose
k=0;
hence thesis by A210,A218,A219,ABSVALUE:2;
end;
suppose
A220: k>0;
Fk1=ADD.(Fk,SFk1) by A211,A217,A220;
then Fk1=Fk+SFk1 by A64;
then Fk1.pp=0+SFk1.pp by A214,A216,A220,NAGATA_1:def 7
,NAT_1:13;
hence thesis by A218,A219,ABSVALUE:2;
end;
end;
A221: R[ 0 ];
for n holds R[n] from NAT_1:sch 2(A221,A213);
hence (ADD"**"SF).pp=0 by A209,A212;
end;
end;
SumFdist.pp=ADD "**" SF by A63;
hence thesis by A205,NAGATA_1:def 8;
end;
thus SumFTS.(p,r)<=SumFTS.(p,q)+SumFTS.(r,q)
proof
reconsider pr=[p,r],pq=[p,q],rq=[r,q] as Point of [:T,T:] by
BORSUK_1:def 2;
reconsider SFpr=SFdist.pr as FinSequence of Fun by FINSEQ_1:def 11;
reconsider ASFpr=ADD"**"SFpr as RealMap of [:T,T:] by FUNCT_2:66;
reconsider SumFpr=SumFdist.pr,SumFpq=SumFdist.pq, SumFrq=SumFdist.rq
as RealMap of [:T,T:] by FUNCT_2:66;
A222: SumFTS.pr = SumFpr.pr & SumFTS.pq = SumFpq.pq by NAGATA_1:def 8;
SumFpr.pq <=SumFpq.pq & SumFpr.rq <=SumFrq.rq by A116;
then
A223: SumFpr.pq + SumFpr.rq <= SumFpq.pq+SumFrq.rq by XREAL_1:7;
A224: now
per cases;
suppose
A225: len SFpr = 0;
A226: ADD is having_a_unity by A64,NAGATA_1:23;
then
A227: ex f being Element of Fun st f is_a_unity_wrt ADD by
SETWISEO:def 2;
ADD"**"SFpr=the_unity_wrt ADD by A225,A226,FINSOP_1:def 1;
then
A228: ADD"**"SFpr is_a_unity_wrt ADD by A227,BINOP_1:def 8;
then ASFpr.pr=0 & ASFpr.pq=0 by A115;
hence ASFpr.pr <= ASFpr.pq + ASFpr.rq by A115,A228;
end;
suppose
A229: len SFpr <> 0;
then len SFpr >=1 by NAT_1:14;
then consider F be sequence of Fun such that
A230: F.1 = SFpr.1 and
A231: for n being Nat
st 0 <> n & n < len SFpr holds F.(n+1)=ADD.(F.n,
SFpr.(n+1)) and
A232: ADD"**"SFpr=F.(len SFpr) by FINSOP_1:def 1;
defpred T[Nat] means
$1<>0 & $1<=len SFpr implies for
F9 be RealMap of [:T,T:] st F9=F.$1 holds F9.pr<=F9.pq+F9.rq;
A233: for k holds T[k] implies T[k+1]
proof
let k;
assume
A234: T[k];
consider x,y be Point of T such that
[x,y]=pr and
A235: rng SFpr=RNG(Fx(x)\/Fx(y)) by A61;
assume that
k+1<>0 and
A236: k+1 <=len SFpr;
A237: k<len SFpr by A236,NAT_1:13;
k+1>=1 by NAT_1:14;
then k+1 in dom SFpr by A236,FINSEQ_3:25;
then SFpr.(k+1) in RNG(Fx(x)\/Fx(y)) by A235,FUNCT_1:def 3;
then consider fd be RealMap of T such that
A238: Fdist.fd =SFpr.(k+1) and
fd in Fx(x)\/Fx(y);
fd in Funcs(cT,REAL) by FUNCT_2:8;
then reconsider
Fdistfd=Fdist.fd, Fk1=F.(k+1), Fk=F.k, SFk1=SFpr.(k
+1) as RealMap of [:T,T:] by A238,FUNCT_2:5,66;
A239: fd.p-fd.r=(fd.p-fd.q)+(fd.q-fd.r);
then
A240: |.fd.p-fd.r.|<=|.fd.p-fd.q.|+ |.fd.q- fd.r.| by COMPLEX1:56;
A241: fd in Funcs(cT,REAL) by FUNCT_2:8;
then
A242: Fdistfd.(p,r)= |.fd.p-fd.r.| & Fdistfd.(p,q)=|.fd.p-
fd.q.| by A46;
A243: |.fd.q-fd.r.|=|.-(fd.q-fd.r).| & Fdistfd.(r,q)=|.fd.
r-fd.q.| by A46,A241,COMPLEX1:52;
let F9 be RealMap of [:T,T:] such that
A244: F9=F.(k+1);
per cases;
suppose
k=0;
hence thesis by A230,A238,A239,A242,A243,A244,COMPLEX1:56;
end;
suppose
A245: k>0;
then Fk.pr<=Fk.pq+Fk.rq by A234,A236,NAT_1:13;
then
A246: Fk.pr+SFk1.pr<=(Fk.pq+Fk.rq)+(SFk1.pq+SFk1.rq) by A238,A240
,A242,A243,XREAL_1:7;
Fk1=ADD.(Fk,SFk1) by A231,A237,A245;
then
A247: Fk1=Fk+SFk1 by A64;
then Fk1.pq=Fk.pq+SFk1.pq & Fk1.rq=Fk.rq+SFk1.rq by
NAGATA_1:def 7;
hence thesis by A244,A247,A246,NAGATA_1:def 7;
end;
end;
A248: T[ 0 ];
for n holds T[n] from NAT_1:sch 2(A248,A233);
hence ASFpr.pr <= ASFpr.pq + ASFpr.rq by A229,A232;
end;
end;
SumFpr=ADD "**" SFpr by A63;
then SumFpr.pr<=SumFpq.pq+SumFrq.rq by A224,A223,XXREAL_0:2;
hence thesis by A222,NAGATA_1:def 8;
end;
end;
then
A249: SumFTS is_a_pseudometric_of cT by NAGATA_1:28;
A250: for p be Point of T,fd be Element of Funcs(cT, REAL) st fd in Fx(p)
holds funcdist[fd,Fdist.fd] & Fdist.fd is continuous RealMap of [:T,T:]
proof
let p be Point of T,fd be Element of Funcs(cT,REAL);
reconsider FD=Fdist.fd as RealMap of [:T,T:] by FUNCT_2:66;
assume fd in Fx(p);
then consider A be Subset of T such that
A251: fd=Fn.A and
A252: A in Bn.n and
A in s(Sx.p);
A253: funcdist[fd,Fdist.fd] by A46;
F[A,Fn.A] by A26,A252;
then FD is continuous by A251,A253,NAGATA_1:21;
hence thesis by A46;
end;
A254: for pq9 holds SumFdist.pq9 is continuous RealMap of [:T,T:]
proof
let pq9;
reconsider SF=SFdist.pq9 as FinSequence of Fun by FINSEQ_1:def 11;
consider p,q such that
[p,q]=pq9 and
A255: rng SF=RNG(Fx(p)\/Fx(q)) by A61;
for n being Element of NAT
st 0<>n & n<=len SF holds SF.n is continuous RealMap of [:T ,T:]
proof
let n be Element of NAT;
assume that
A256: 0<>n and
A257: n<=len SF;
n>=1 by A256,NAT_1:14;
then n in dom SF by A257,FINSEQ_3:25;
then SF.n in RNG(Fx(p)\/Fx(q)) by A255,FUNCT_1:def 3;
then consider fd be RealMap of T such that
A258: SF.n=Fdist.fd and
A259: fd in (Fx(p)\/Fx(q));
A260: fd in Funcs(cT,REAL) by FUNCT_2:8;
fd in Fx(p) or fd in Fx(q) by A259,XBOOLE_0:def 3;
hence thesis by A250,A258,A260;
end;
then ADD"**"SF is continuous RealMap of [:T,T:] by A64,NAGATA_1:25;
hence thesis by A63;
end;
A261: for pq9 holds SumFdist9.pq9 is continuous Function of [:T,T:],R^1
proof
let pq9;
reconsider SF=SumFdist.pq9 as Function of [:T,T:],R^1 by A254,
TOPMETR:17;
SumFdist.pq9 is continuous RealMap of [:T,T:] by A254;
then SF is continuous by JORDAN5A:27;
hence thesis;
end;
take min(jj,SumFTS9);
A262: for p,q holds min(jj,SumFTS9).[p,q]<=1
proof
let p,q;
cTT=[:cT,cT:] by BORSUK_1:def 2;
then min(jj,SumFTS9).[p,q]=min(1,SumFTS9.[p,q]) by NAGATA_1:def 9;
hence thesis by XXREAL_0:17;
end;
for p,q be Point of [:T,T:] st p in SS.q holds SumFdist9.p.p=
SumFdist9.q.p by A116;
then SumFdist9 Toler is continuous by A261,A35,NAGATA_1:26;
then SumFTS9 is continuous by JORDAN5A:27;
then min(jj,SumFTS9)=min(jj,SumFTS) & min(jj,SumFTS9) is continuous by
BORSUK_1:def 2,NAGATA_1:27;
hence thesis by A249,A262,A113,NAGATA_1:30;
end;
A263: for k be object st k in NAT
ex f be object st f in Funcs(cTT,REAL) & N[k,f ]
proof
A264: NAT =rng PairFunc by Th2,FUNCT_2:def 3;
let k be object;
assume k in NAT;
then consider nm be object such that
A265: nm in dom PairFunc and
A266: k=PairFunc.nm by A264,FUNCT_1:def 3;
consider n,m be object such that
A267: n in NAT & m in NAT and
A268: nm=[n,m] by A265,ZFMISC_1:def 2;
consider pmet9 such that
A269: NN[n,m,pmet9] by A7,A267;
take pmet9;
thus pmet9 in Funcs(cTT,REAL) by FUNCT_2:8;
take pm = pmet9;
thus pm = pmet9;
let n1,m1 be Nat;
assume PairFunc".k=[n1,m1];
then [n1,m1]=[n,m] by A265,A266,A268,Lm2,Th2,FUNCT_1:32;
then n1=n & m1=m by XTUPLE_0:1;
hence thesis by A269;
end;
consider F be sequence of Funcs(cTT,REAL) such that
A270: for n be object st n in NAT holds N[n,F.n] from FUNCT_2:sch 1(A263);
A271: now
let n be Nat;
[:cT,cT:]=cTT by BORSUK_1:def 2;
hence F.n is PartFunc of [:cT,cT:],REAL by FUNCT_2:66;
end;
dom F=NAT by FUNCT_2:def 1;
then reconsider F9=F as Functional_Sequence of[:cT,cT:],REAL by A271,
SEQFUNC:1;
A272: for p,A9 st not p in A9 & A9 is closed ex k st for pmet st F9.k=pmet
holds lower_bound(pmet,A9).p>0
proof
let p,A9 such that
A273: not p in A9 and
A274: A9 is closed;
set O=A9`;
p in O by A273,XBOOLE_0:def 5;
then consider U be Subset of T such that
A275: p in U and
A276: Cl U c=O and
A277: U in Union Bn by A1,A5,A274,NAGATA_1:19;
Union Bn c=the topology of T by A5,TOPS_2:64;
then reconsider U as open Subset of T by A277,PRE_TOPC:def 2;
consider n such that
A278: U in Bn.n by A277,PROB_1:12;
consider W be Subset of T such that
A279: p in W & Cl W c=U and
A280: W in Union Bn by A1,A5,A275,NAGATA_1:19;
Union Bn c=the topology of T by A5,TOPS_2:64;
then reconsider W as open Subset of T by A280,PRE_TOPC:def 2;
consider m such that
A281: W in Bn.m by A280,PROB_1:12;
set k=PairFunc.[n,m];
A282: k in NAT by ORDINAL1:def 12;
A283: n in NAT & m in NAT by ORDINAL1:def 12;
consider G be RealMap of [:T,T:] such that
A284: G = F.k and
A285: for n,m being Nat st PairFunc".k=[n,m]
holds NN[n,m,G] by A270,A282;
A286: [n,m] in [:NAT,NAT:] by A283,ZFMISC_1:87;
reconsider kk=k as Element of NAT by ORDINAL1:def 12;
dom PairFunc = [:NAT,NAT:] by FUNCT_2:def 1;
then [n,m]=PairFunc".kk by Lm2,Th2,FUNCT_1:32,A286;
then consider pmet such that
A287: G=pmet and
G is continuous and
pmet is_a_pseudometric_of cT and
A288: for p,q holds pmet.[p,q]<=1 & for p,q st ex A,B st A is open &
B is open & A in Bn.m & B in Bn.n & p in A & Cl A c= B & not q in B holds pmet.
[p,q] = 1 by A285;
A289: for rn st rn in (dist(pmet,p)).:A9 holds rn>=1
proof
let rn;
assume rn in (dist(pmet,p)).:A9;
then consider a be object such that
A290: a in dom dist(pmet,p) and
A291: a in A9 and
A292: rn=(dist(pmet,p)).a by FUNCT_1:def 6;
reconsider a as Point of T by A290;
A293: pmet.(p,a)=dist(pmet,p).a by Def2;
U c= Cl U by PRE_TOPC:18;
then U c= O by A276;
then U misses A9 by SUBSET_1:23;
then not a in U by A291,XBOOLE_0:3;
hence thesis by A279,A278,A281,A288,A292,A293;
end;
take k;
cT=dom dist(pmet,p) by FUNCT_2:def 1;
then lower_bound ((dist(pmet,p)).:A9) >= 1 by A289,SEQ_4:43;
hence thesis by A284,A287,Def3;
end;
for k ex pmet st F9.k=pmet & pmet is_a_pseudometric_of cT & (for pq
holds pmet.pq<=1) & for pmet9 st pmet=pmet9 holds pmet9 is continuous
proof
let k;
A294: k in NAT by ORDINAL1:def 12;
then consider Fk be RealMap of [:T,T:] such that
A295: Fk = F.k and
A296: for n,m st PairFunc".k=[n,m] holds NN[n,m,Fk] by A270;
NAT =rng PairFunc by Th2,FUNCT_2:def 3;
then consider nm be object such that
A297: nm in dom PairFunc and
A298: k=PairFunc.nm by FUNCT_1:def 3,A294;
consider n,m be object such that
A299: n in NAT & m in NAT and
A300: nm=[n,m] by A297,ZFMISC_1:def 2;
[n,m]=PairFunc".k by A297,A298,A300,Lm2,Th2,FUNCT_1:32;
then consider pmet such that
A301: Fk=pmet and
A302: Fk is continuous and
A303: pmet is_a_pseudometric_of cT and
A304: for p,q holds pmet.[p,q]<=1 & for p,q st ex A,B st A is open &
B is open & A in Bn.m & B in Bn.n & p in A & Cl A c= B & not q in B holds pmet.
[p,q] = 1 by A299,A296;
take pmet;
thus F9.k=pmet & pmet is_a_pseudometric_of cT by A295,A301,A303;
thus for pq holds pmet.pq<=1
proof
let pq;
ex p,q be object st p in cT & q in cT & pq=[p,q] by ZFMISC_1:def 2;
hence thesis by A304;
end;
thus thesis by A301,A302;
end;
hence thesis by A2,A272,Th17;
end;
thus thesis by NAGATA_1:15,16;
end;
theorem Th20:
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
proof
set cT=the carrier of T;
assume T is metrizable;
then consider metr be Function of [:cT,cT:],REAL such that
A1: metr is_metric_of cT and
A2: Family_open_set(SpaceMetr(cT,metr))=the topology of T by PCOMPS_1:def 8;
reconsider PM=SpaceMetr(cT,metr) as non empty MetrSpace by A1,PCOMPS_1:36;
set cPM= the carrier of PM;
let FX be Subset-Family of T such that
A3: FX is Cover of T and
A4: FX is open;
defpred P1[set] means $1 in FX;
deffunc F1(Point of PM,Nat)=Ball($1,1/(2|^($2+1)));
consider R be Relation such that
A5: R well_orders FX by WELLORD2:17;
consider Mn be Relation such that
A6: Mn = R |_2 FX;
set UB ={union {Ball(c,1/2) where c is Point of PM: c in V\PartUnion(V,Mn) &
Ball(c,3/2) c= V} where V is Subset of PM:V in FX};
UB c= bool the carrier of PM
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in UB;
then consider V be Subset of PM such that
A7: x=union{Ball(c,1/2) where c is Point of PM: c in V\PartUnion(V,Mn
) & Ball(c,3/2)c= V} and
V in FX;
xx c= cPM
proof
let y be object;
assume y in xx;
then consider W be set such that
A8: y in W and
A9: W in {Ball(c,1/2) where c is Point of PM: c in V\PartUnion(V,Mn
)& Ball(c,3/2)c=V} by A7,TARSKI:def 4;
ex c be Point of PM st W=Ball(c,1/2) & c in V\PartUnion(V,Mn)& Ball
(c,3/2) c= V by A9;
hence thesis by A8;
end;
hence thesis;
end;
then reconsider UB as Subset-Family of PM;
defpred Q1[Point of PM,Subset of PM,Nat] means $1 in $2\PartUnion($2,Mn) &
Ball($1,3/(2|^($3+1)))c= $2;
consider Un be sequence of bool bool cPM such that
A10: Un.0 = UB &
for n being Nat holds Un.(n+1)= {union{F1(c,n) where c is Point
of PM:Q1[c,V,n] &
not c in union{union (Un.k) where k is Nat: k <= n}}
where V is Subset of PM
: P1[V]} from PCOMPS_2:sch 3;
reconsider Un9=Un as FamilySequence of T by A1,PCOMPS_2:4;
take Un9;
thus Union Un9 is open
proof
let A;
assume A in Union Un9;
then consider n such that
A11: A in Un.n by PROB_1:12;
per cases;
suppose
n=0;
then consider V be Subset of PM such that
A12: A=union{Ball(c,1/2) where c is Point of PM: c in V\PartUnion(V,
Mn) & Ball(c,3/2) c= V} and
V in FX by A10,A11;
set BALL={Ball(c,1/2) where c is Point of PM: c in V\PartUnion(V,Mn) &
Ball(c,3/2) c= V};
BALL c= bool the carrier of PM
proof
let x be object;
assume x in BALL;
then ex c be Point of PM st x=Ball(c,1/2) & c in V\PartUnion(V,Mn )&
Ball(c,3/2) c= V;
hence thesis;
end;
then reconsider BALL as Subset-Family of PM;
BALL c= Family_open_set PM
proof
let x be object;
assume x in BALL;
then ex c be Point of PM st x=Ball(c,1/2) & c in V\PartUnion(V,Mn )&
Ball(c,3/2) c= V;
hence thesis by PCOMPS_1:29;
end;
then A in the topology of T by A2,A12,PCOMPS_1:32;
hence thesis by PRE_TOPC:def 2;
end;
suppose
n>0;
then consider m being Nat such that
A13: n=m+1 by NAT_1:6;
reconsider m as Element of NAT by ORDINAL1:def 12;
A in {union{F1(c,m) where c is Point of PM:Q1[c,V,m]& not c in
union{union (Un.k) where k is Nat: k <= m}}
where V is Subset of PM: P1[V]} by A10,A11,A13;
then consider V be Subset of PM such that
A14: A=union{F1(c,m) where c is Point of PM:Q1[c,V,m]& not c in
union{union (Un.k) where k is Nat: k <= m}} & P1[V];
set BALL={F1(c,m) where c is Point of PM:Q1[c,V,m]& not c in union{union
(Un.k) where k is Nat: k <= m}};
BALL c= bool the carrier of PM
proof
let x be object;
assume x in BALL;
then ex c be Point of PM st x=F1(c,m) & Q1[c,V,m] & not c in union{
union (Un.k) where k is Nat: k <= m};
hence thesis;
end;
then reconsider BALL as Subset-Family of PM;
BALL c= Family_open_set PM
proof
let x be object;
assume x in BALL;
then ex c be Point of PM st x=F1(c,m) & Q1[c,V,m] & not c in union{
union (Un.k) where k is Nat: k <= m};
hence thesis by PCOMPS_1:29;
end;
then A in the topology of T by A2,A14,PCOMPS_1:32;
hence thesis by PRE_TOPC:def 2;
end;
end;
A15: Mn well_orders FX by A5,A6,PCOMPS_2:1;
[#]T c= union Union Un9
proof
let x be object such that
A16: x in [#]T;
reconsider x9=x as Element of PM by A1,A16,PCOMPS_2:4;
defpred P2[set] means x in $1;
ex G be Subset of T st x in G & G in FX by A3,A16,PCOMPS_1:3;
then
A17: ex G be set st G in FX & P2[G];
consider X such that
A18: X in FX & P2[X] & for Y be set st Y in FX & P2[Y] holds [X,Y] in
Mn from PCOMPS_2:sch 1(A15,A17);
assume
A19: not x in union Union Un9;
A20: for V be set,n be Nat st V in Un9.n holds not x in V
proof
let V be set,n be Nat;
assume V in Un9.n;
then V in Union Un by PROB_1:12;
hence thesis by A19,TARSKI:def 4;
end;
A21: for n holds not x in union (Un9.n)
proof
let n;
assume x in union (Un9.n);
then ex V be set st x in V & V in Un9.n by TARSKI:def 4;
hence contradiction by A20;
end;
reconsider X as Subset of T by A18;
X is open by A4,A18;
then
A22: X in Family_open_set PM by A2,PRE_TOPC:def 2;
reconsider X as Subset of PM by A1,PCOMPS_2:4;
consider r such that
A23: r>0 and
A24: Ball(x9,r) c= X by A18,A22,PCOMPS_1:def 4;
defpred P3[Nat] means 3/(2 |^ $1) <= r;
ex k st P3[k] by A23,PREPOWER:92;
then
A25: ex k be Nat st P3[k];
consider k be Nat such that
A26: P3[k] & for i be Nat st P3[i] holds k <= i from NAT_1:sch 5(A25);
set W=union{F1(y,k) where y is Point of PM:Q1[y,X,k] & not y in union{
union(Un.i) where i is Nat:i <= k}};
2|^(k+1)=2|^k*2 by NEWTON:6;
then 2|^k > 0 & 2|^(k+1) >= 2|^k by PREPOWER:6,XREAL_1:151;
then 3/2 |^(k+1) <= 3/2|^k by XREAL_1:118;
then
A27: 3/2 |^(k+1) <= r by A26,XXREAL_0:2;
A28: x in W
proof
not x9 in PartUnion(X,Mn)
proof
assume x9 in PartUnion(X,Mn);
then x9 in union (Mn-Seg(X)) by PCOMPS_2:def 1;
then consider M be set such that
A29: x9 in M and
A30: M in Mn-Seg(X) by TARSKI:def 4;
A31: M <> X by A30,WELLORD1:1;
A32: Mn is_antisymmetric_in FX by A15,WELLORD1:def 5;
A33: [M,X] in Mn by A30,WELLORD1:1;
then M in field Mn by RELAT_1:15;
then
A34: M in FX by A5,A6,PCOMPS_2:1;
then [X,M] in Mn by A18,A29;
hence contradiction by A18,A31,A33,A34,A32,RELAT_2:def 4;
end;
then
A35: x9 in X\PartUnion(X,Mn) by A18,XBOOLE_0:def 5;
set A=Ball(x9,1/(2|^(k+1)));
0 < 2|^(k+1) by PREPOWER:6;
then
A36: x9 in A by TBSP_1:11,XREAL_1:139;
A37: not x9 in union{union(Un9.i) where i is Nat:i <= k}
proof
assume x9 in
union {union(Un9.i) where i is Nat:i <= k};
then consider D be set such that
A38: x9 in D & D in {union(Un9.i) where i is Nat:i <= k}
by TARSKI:def 4;
ex i being Nat st D=union (Un9.i) & i <= k by A38;
hence contradiction by A21,A38;
end;
Ball(x9,3/(2|^(k+1))) c= Ball(x9,r) by A27,PCOMPS_1:1;
then Ball(x9,3/(2|^(k+1))) c= X by A24;
then A in {F1(y,k) where y is Point of PM:Q1[y,X,k] & not y in union {
union(Un9.i) where i is Nat: i <= k}} by A35,A37;
hence thesis by A36,TARSKI:def 4;
end;
k in NAT & W in {union{F1(y,k)where y is Point of PM: Q1[y,V,k] & not
y in union {union(Un.q) where q is Nat: q <= k}}
where V is Subset
of PM: V in FX} by A18,ORDINAL1:def 12;
then W in Un9.(k+1) by A10;
hence thesis by A20,A28;
end;
then [#]T = union Union Un9;
hence Union Un9 is Cover of T by SETFAM_1:45;
for X be set st X in Union Un9 ex Y be set st Y in FX & X c= Y
proof
let X be set;
assume X in Union Un9;
then consider n such that
A39: X in Un.n by PROB_1:12;
per cases;
suppose
n=0;
then consider V be Subset of PM such that
A40: X=union{Ball(c,1/2) where c is Point of PM: c in V\PartUnion(V,
Mn) & Ball(c,3/2) c= V} and
A41: V in FX by A10,A39;
set BALL={Ball(c,1/2) where c is Point of PM: c in V\PartUnion(V,Mn) &
Ball(c,3/2) c= V};
BALL c= bool the carrier of PM
proof
let x be object;
assume x in BALL;
then ex c be Point of PM st x=Ball(c,1/2) & c in V\PartUnion(V,Mn) &
Ball(c,3/2) c= V;
hence thesis;
end;
then reconsider BALL as Subset-Family of PM;
for W be set st W in BALL holds W c= V
proof
let W be set;
assume W in BALL;
then consider c be Element of PM such that
A42: W=Ball(c,1/2) and
c in V\PartUnion(V,Mn) and
A43: Ball(c,3/2) c= V;
Ball(c,1/2) c= Ball(c,3/2) by PCOMPS_1:1;
hence thesis by A42,A43;
end;
then X c= V by A40,ZFMISC_1:76;
hence thesis by A41;
end;
suppose
n>0;
then consider m being Nat such that
A44: n=m+1 by NAT_1:6;
reconsider m as Element of NAT by ORDINAL1:def 12;
X in {union{F1(c,m) where c is Point of PM:Q1[c,V,m] & not c in
union{union (Un.k) where k is Nat: k <= m}}
where V is Subset of PM: P1[V]} by A10,A39,A44;
then consider V be Subset of PM such that
A45: X=union{F1(c,m) where c is Point of PM:Q1[c,V,m] & not c in
union{union (Un.k) where k is Nat: k <= m}} & P1[V];
set BALL={F1(c,m) where c is Point of PM:Q1[c,V,m] & not c in union{
union (Un.k) where k is Nat: k <= m}};
BALL c= bool the carrier of PM
proof
let x be object;
assume x in BALL;
then ex c be Point of PM st x=F1(c,m) & Q1[c,V,m] & not c in union{
union (Un.k) where k is Nat: k <= m};
hence thesis;
end;
then reconsider BALL as Subset-Family of PM;
for W be set st W in BALL holds W c= V
proof
let W be set;
assume W in BALL;
then consider c be Element of PM such that
A46: W=F1(c,m) & Q1[c,V,m] &
not c in union{union (Un.k) where k is Nat: k <= m};
0 < 2|^(m+1) by PREPOWER:6;
then 1/(2|^(m+1)) < 3/(2|^(m+1)) by XREAL_1:74;
then F1(c,m)c=Ball(c,3/(2|^(m+1))) by PCOMPS_1:1;
hence thesis by A46,XBOOLE_1:1;
end;
then X c= V by A45,ZFMISC_1:76;
hence thesis by A45;
end;
end;
hence Union Un9 is_finer_than FX by SETFAM_1:def 2;
for n being Element of NAT holds Un9.n is discrete
proof
let n be Element of NAT;
for p ex O be open Subset of T st p in O & for A,B st A in Un9.n & B
in Un9.n holds O meets A & O meets B implies A=B
proof
let p;
reconsider p9=p as Point of PM by A1,PCOMPS_2:4;
set O=Ball(p9,1/(2|^(n+2)));
O in Family_open_set PM by PCOMPS_1:29;
then reconsider O as open Subset of T by A2,PRE_TOPC:def 2;
take O;
A47: now
let A,B such that
A48: A in Un9.n and
A49: B in Un9.n;
assume that
A50: O meets A and
A51: O meets B;
consider a be object such that
A52: a in O and
A53: a in A by A50,XBOOLE_0:3;
consider b be object such that
A54: b in O and
A55: b in B by A51,XBOOLE_0:3;
reconsider a,b as Point of PM by A52,A54;
A56: dist(p9,b)<1/(2|^(n+2)) by A54,METRIC_1:11;
A57: dist(a,b)<=dist(a,p9)+dist(p9,b) & 2|^(n+1+1)=2|^(n+1)*2 by METRIC_1:4
,NEWTON:6;
dist(p9,a)<1/(2|^(n+2)) by A52,METRIC_1:11;
then dist(a,p9)+dist(p9,b)<1/(2|^(n+2))+1/(2|^(n+2)) by A56,XREAL_1:8;
then dist(a,b)<2*(1/(2*2|^(n+1))) by A57,XXREAL_0:2;
then dist(a,b)<(2*1) /(2*2|^(n+1)) by XCMPLX_1:74;
then
A58: dist(a,b)<(2/2*1)/2|^(n+1) by XCMPLX_1:83;
now
per cases;
suppose
A59: n=0;
then
A60: dist(a,b)<1/2 by A58;
consider V be Subset of PM such that
A61: A=union {Ball(c,1/2) where c is Point of PM: c in V\
PartUnion(V,Mn) & Ball(c,3/2) c= V} and
A62: V in FX by A10,A48,A59;
consider Ba be set such that
A63: a in Ba and
A64: Ba in {Ball(c,1/2) where c is Point of PM: c in V\
PartUnion(V,Mn) & Ball(c,3/2) c= V} by A53,A61,TARSKI:def 4;
consider ca be Point of PM such that
A65: Ba=Ball(ca,1/2) and
A66: ca in V\PartUnion(V,Mn) and
A67: Ball(ca,3/2) c= V by A64;
dist(ca,a)<1/2 by A63,A65,METRIC_1:11;
then
A68: dist(ca,a)+dist(a,b)<1/2+1/2 by A60,XREAL_1:8;
dist(ca,b)<=dist(ca,a)+ dist(a,b) by METRIC_1:4;
then
A69: dist(ca,b)<1 by A68,XXREAL_0:2;
consider W be Subset of PM such that
A70: B=union {Ball(c,1/2) where c is Point of PM: c in W\
PartUnion(W,Mn) & Ball(c,3/2) c= W} and
A71: W in FX by A10,A49,A59;
consider Bb be set such that
A72: b in Bb and
A73: Bb in {Ball(c,1/2) where c is Point of PM: c in W\
PartUnion(W,Mn) & Ball(c,3/2) c= W} by A55,A70,TARSKI:def 4;
consider cb be Point of PM such that
A74: Bb=Ball(cb,1/2) and
A75: cb in W\PartUnion(W,Mn) and
A76: Ball(cb,3/2) c= W by A73;
A77: dist(ca,cb)<=dist(ca,b)+ dist(b,cb) by METRIC_1:4;
dist(cb,b)<1/2 by A72,A74,METRIC_1:11;
then dist(ca,b)+dist(b,cb)<1+1/2 by A69,XREAL_1:8;
then dist(ca,cb)<3/2 by A77,XXREAL_0:2;
then
A78: ca in Ball(cb,3/2) & cb in Ball(ca,3/2) by METRIC_1:11;
V=W
proof
assume
A79: V<>W;
Mn is_connected_in FX by A15,WELLORD1:def 5;
then [V,W] in Mn or [W,V] in Mn by A62,A71,A79,RELAT_2:def 6;
then V in Mn-Seg(W) or W in Mn-Seg(V)by A79,WELLORD1:1;
then cb in union(Mn-Seg(W)) or ca in union(Mn-Seg(V)) by A67,A76
,A78,TARSKI:def 4;
then cb in PartUnion(W,Mn) or ca in PartUnion(V,Mn) by
PCOMPS_2:def 1;
hence thesis by A66,A75,XBOOLE_0:def 5;
end;
hence A=B by A61,A70;
end;
suppose
n>0;
then consider m being Nat such that
A80: n=m+1 by NAT_1:6;
set r=1/(2|^n);
A81: 3*r=(3*1)/2|^n by XCMPLX_1:74;
2|^(n+1)=2|^n*2 by NEWTON:6;
then 2|^n>0 & 2|^(n+1)>=2|^n by PREPOWER:6,XREAL_1:151;
then 1/2|^(n+1) <= r by XREAL_1:118;
then
A82: dist(a,b)<r by A58,XXREAL_0:2;
reconsider m as Element of NAT by ORDINAL1:def 12;
A in {union{F1(c,m) where c is Point of PM:Q1[c,V,m] & not c
in union{union (Un.k) where k is Nat: k <= m}}
where V is Subset of PM: P1[V]} by A10,A48,A80;
then consider V be Subset of PM such that
A83: A=union{F1(c,m) where c is Point of PM:Q1[c,V,m] & not c
in union{union(Un.k) where k is Nat: k <= m}}
& P1[V];
consider Ba be set such that
A84: a in Ba&Ba in {F1(c,m) where c is Point of PM:Q1[c,V,m]
& not c in union{union(Un.k) where k is Nat: k <= m}}
by A53,A83,TARSKI:def 4;
consider ca be Point of PM such that
A85: Ba=F1(ca,m) & Q1[ca,V,m] &
not ca in union{union(Un.k) where k is Nat:k
<=m} by A84;
dist(ca,a)<r by A80,A84,A85,METRIC_1:11;
then
A86: dist(ca,a)+dist(a,b)<r+r by A82,XREAL_1:8;
dist(ca,b)<=dist(ca,a)+ dist(a,b) by METRIC_1:4;
then
A87: dist(ca,b)<r+r by A86,XXREAL_0:2;
B in {union{F1(c,m) where c is Point of PM:Q1[c,W,m] & not c
in union{union (Un.k) where k is Nat: k <= m}}
where W is Subset of PM:P1[W]} by A10,A49,A80;
then consider W be Subset of PM such that
A88: B=union{F1(c,m) where c is Point of PM:Q1[c,W,m] & not c
in union{union(Un.k) where k is Nat: k <= m}} & P1[W];
consider Bb be set such that
A89: b in Bb&Bb in {F1(c,m) where c is Point of PM:Q1[c,W,m]
& not c in union{union(Un.k) where k is Nat: k <= m}}
by A55,A88,TARSKI:def 4;
consider cb be Point of PM such that
A90: Bb=F1(cb,m) & Q1[cb,W,m] &
not cb in union{union(Un.k) where k is Nat:k
<=m} by A89;
A91: dist(ca,cb)<=dist(ca,b)+ dist(b,cb) by METRIC_1:4;
dist(cb,b)<r by A80,A89,A90,METRIC_1:11;
then dist(ca,b)+dist(b,cb)<(r+r)+r by A87,XREAL_1:8;
then dist(ca,cb)<3*r by A91,XXREAL_0:2;
then
A92: ca in Ball(cb,3/2|^(m+1)) & cb in Ball(ca,3/2|^( m+1)) by A80,A81,
METRIC_1:11;
V=W
proof
assume
A93: V<>W;
Mn is_connected_in FX by A15,WELLORD1:def 5;
then [V,W] in Mn or [W,V] in Mn by A83,A88,A93,RELAT_2:def 6;
then V in Mn-Seg(W) or W in Mn-Seg(V)by A93,WELLORD1:1;
then cb in union(Mn-Seg(W)) or ca in union(Mn-Seg(V)) by A85,A90
,A92,TARSKI:def 4;
then cb in PartUnion(W,Mn) or ca in PartUnion(V,Mn) by
PCOMPS_2:def 1;
hence thesis by A85,A90,XBOOLE_0:def 5;
end;
hence A=B by A83,A88;
end;
end;
hence A=B;
end;
0 < 2|^(n+2) by PREPOWER:6;
hence thesis by A47,TBSP_1:11,XREAL_1:139;
end;
hence thesis by NAGATA_1:def 1;
end;
hence Un9 is sigma_discrete by NAGATA_1:def 2;
end;
theorem Th21:
for T st T is metrizable ex Un be FamilySequence of T st Un is
Basis_sigma_discrete
proof
let T such that
A1: T is metrizable;
consider metr be Function of [:the carrier of T,the carrier of T:],REAL such
that
A2: metr is_metric_of the carrier of T and
A3: Family_open_set(SpaceMetr (the carrier of T,metr)) = the topology of
T by A1,PCOMPS_1:def 8;
set bbcT=bool bool the carrier of T;
reconsider PM = SpaceMetr(the carrier of T,metr) as non empty MetrSpace by A2
,PCOMPS_1:36;
deffunc BALL(object)=
{Ball(x, 1/(2 |^ (In($1,NAT)))) where x is Point of PM: x
is Point of PM};
A4: for k be object st k in NAT holds BALL(k) in bool bool the carrier of T
proof
let k be object;
assume k in NAT;
then reconsider k as Element of NAT;
BALL(k) c= bool the carrier of T
proof
let B be object;
assume B in BALL(k);
then ex x be Point of PM st B=Ball(x,1/(2|^k)) & x is Point of PM;
then B in Family_open_set PM by PCOMPS_1:29;
hence thesis by A3;
end;
hence thesis;
end;
consider FB be FamilySequence of T such that
A5: for k be object st k in NAT holds FB.k= BALL(k) from FUNCT_2:sch 2(A4);
defpred U[set,set] means ex FS be FamilySequence of T st $2 = FS & Union FS
is open & Union FS is Cover of T & Union FS is_finer_than FB.$1 & FS is
sigma_discrete;
set TPM = TopSpaceMetr PM;
A6: TPM = TopStruct (#the carrier of PM,Family_open_set PM#) by PCOMPS_1:def 5;
then
A7: [#]T=[#]TPM by A2,PCOMPS_2:4;
A8: for n be Element of NAT ex Un be Element of Funcs(NAT,bbcT) st U[n,Un]
proof
let n be Element of NAT;
now
let U be Subset of T;
assume U in (FB.n);
then U in BALL(n) by A5;
then ex x be Point of PM st U = Ball(x,1/(2|^ n)) & x is Point of PM;
then U in the topology of T by A3,PCOMPS_1:29;
hence U is open by PRE_TOPC:def 2;
end;
then
A9: FB.n is open;
A10: [#]TPM c= union (FB.n)
proof
let x be object;
assume x in [#]TPM;
then reconsider x9=x as Element of PM by A6;
2|^n > 0 by NEWTON:83;
then
A11: x9 in Ball(x9,1/(2|^ n)) by TBSP_1:11,XREAL_1:139;
Ball(x9,1/(2|^ n)) in BALL(n);
then Ball(x9,1/(2|^ n)) in FB.n by A5;
hence thesis by A11,TARSKI:def 4;
end;
union (FB.n) c= [#]TPM
proof
given x being object such that
A12: x in union (FB.n) and
A13: not x in [#]TPM;
consider A be set such that
A14: x in A and
A15: A in (FB.n) by A12,TARSKI:def 4;
A in BALL(n) by A5,A15;
then
ex y be Point of PM st A=Ball(y,1/(2|^n)) & y is Point of PM;
hence thesis by A6,A13,A14;
end;
then [#]TPM = union (FB.n) by A10;
then (FB.n) is Cover of T by A7,SETFAM_1:45;
then consider Un be FamilySequence of T such that
A16: Union Un is open & Union Un is Cover of T & Union Un
is_finer_than FB. n & Un is sigma_discrete by A1,A9,Th20;
Un in Funcs(NAT,bbcT) by FUNCT_2:8;
hence thesis by A16;
end;
consider Un be sequence of Funcs(NAT,bbcT) such that
A17: for n be Element of NAT holds U[n,Un.n] from FUNCT_2:sch 3(A8);
defpred X[object,object] means
for n,m st PairFunc.[n,m]=$1 for Unn be
FamilySequence of T st Unn=Un.n holds $2=Unn.m;
A18: for k be object st k in NAT ex Ux be object st Ux in bbcT & X[k,Ux]
proof
let k be object;
assume k in NAT;
then reconsider k9=k as Element of NAT;
NAT =rng PairFunc by Th2,FUNCT_2:def 3;
then consider nm be object such that
A19: nm in dom PairFunc and
A20: k9=PairFunc.nm by FUNCT_1:def 3;
consider n,m be object such that
A21: n in NAT and
A22: m in NAT and
A23: nm=[n,m] by A19,ZFMISC_1:def 2;
reconsider Unn=Un.n as FamilySequence of T by A21,FUNCT_2:5,66;
take Ux=Unn.m;
dom Unn = NAT by PARTFUN1:def 2;
then m in dom Unn by A22;
then Ux in rng Unn by FUNCT_1:3;
hence Ux in bbcT;
let n1,m1 be Nat such that
A24: PairFunc.[n1,m1]=k;
reconsider nn1=n1,mm1=m1 as Element of NAT by ORDINAL1:def 12;
now
let Unn be FamilySequence of T such that
A25: Unn=Un.nn1;
A26: [n,m]=[nn1,mm1] by A19,A20,A23,A24,Th2,FUNCT_2:19;
then n1=n by XTUPLE_0:1;
hence Ux=Unn.mm1 by A25,A26,XTUPLE_0:1;
end;
hence for Unn be FamilySequence of T st Unn=Un.n1 holds Ux=Unn.m1;
end;
consider UX be sequence of bbcT such that
A27: for k be object st k in NAT holds X[k,UX.k] from FUNCT_2:sch 1(A18);
A28: for A st A is open for p st p in A ex B st B in Union UX & p in B & B c= A
proof
let A;
assume A is open;
then
A29: A in Family_open_set PM by A3,PRE_TOPC:def 2;
let p such that
A30: p in A;
reconsider p as Element of PM by A30,A29;
consider r such that
A31: r>0 and
A32: Ball(p,r) c=A by A30,A29,PCOMPS_1:def 4;
consider n such that
A33: 1/(2|^n)<=r by A31,PREPOWER:92;
consider Unn1 be FamilySequence of T such that
A34: Un.(n+1) = Unn1 and
Union Unn1 is open and
A35: Union Unn1 is Cover of T and
A36: Union Unn1 is_finer_than FB.(n+1) and
Unn1 is sigma_discrete by A17;
union (Union Unn1) = [#]T by A35,SETFAM_1:45;
then consider B be set such that
A37: p in B and
A38: B in (Union Unn1) by TARSKI:def 4;
reconsider B as Subset of PM by A2,A38,PCOMPS_2:4;
consider B1 be set such that
A39: B1 in FB.(n+1) and
A40: B c= B1 by A36,A38,SETFAM_1:def 2;
consider k such that
A41: B in Unn1.k by A38,PROB_1:12;
n + 1 = In(n+1,NAT) & B1 in BALL(n+1) by A5,A39;
then consider q be Point of PM such that
A42: B1=Ball(q,(1/(2|^(n+1)))) and
q is Element of PM;
now
let s be Element of PM;
assume s in B;
then
A43: dist(q,s)<1/(2|^(n+1)) by A40,A42,METRIC_1:11;
dist(q,p)<1/(2|^(n+1)) by A37,A40,A42,METRIC_1:11;
then dist(p,s)<=dist(q,p)+dist(q,s) & dist(q,p)+dist(q,s)<1/(2|^(n+1))+
1/(2|^(n+1 )) by A43,METRIC_1:4,XREAL_1:8;
then dist(p,s)<2*(1/(2|^(n+1))) by XXREAL_0:2;
then dist(p,s)<(1/(2|^n * 2))*2 by NEWTON:6;
then dist(p,s)<(1/(2|^n)) by XCMPLX_1:92;
then dist(p,s)<r by A33,XXREAL_0:2;
hence s in Ball(p,r) by METRIC_1:11;
end;
then
A44: B c= Ball(p,r);
reconsider kk= k as Element of NAT by ORDINAL1:def 12;
UX.(PairFunc.[n+1,kk])=Unn1.kk by A27,A34;
then B in Union UX by A41,PROB_1:12;
hence thesis by A32,A37,A44,XBOOLE_1:1;
end;
for k being Element of NAT holds UX.k is discrete
proof
let k;
A45: k in NAT by ORDINAL1:def 12;
NAT = rng PairFunc by Th2,FUNCT_2:def 3;
then consider nm be object such that
A46: nm in dom PairFunc and
A47: k=PairFunc.nm by FUNCT_1:def 3,A45;
consider n,m be object such that
A48: n in NAT and
A49: m in NAT and
A50: nm=[n,m] by A46,ZFMISC_1:def 2;
consider FS be FamilySequence of T such that
A51: Un.n = FS and
Union FS is open and
Union FS is Cover of T and
Union FS is_finer_than FB.n and
A52: FS is sigma_discrete by A17,A48;
dom FS = NAT by PARTFUN1:def 2;
then m in dom FS by A49;
then FS.m in rng FS by FUNCT_1:3;
then FS.m in bbcT;
then reconsider FSm = FS.m as Subset-Family of T;
FSm is discrete by A49,A52,NAGATA_1:def 2;
hence thesis by A27,A47,A48,A49,A50,A51;
end;
then
A53: UX is sigma_discrete by NAGATA_1:def 2;
Union UX c= the topology of T
proof
let UXk be object;
assume UXk in Union UX;
then consider k such that
A54: UXk in UX.k by PROB_1:12;
reconsider UXk9=UXk as Subset of T by A54;
A55: k in NAT by ORDINAL1:def 12;
NAT =rng PairFunc by Th2,FUNCT_2:def 3;
then consider nm be object such that
A56: nm in dom PairFunc and
A57: k=PairFunc.nm by FUNCT_1:def 3,A55;
consider n,m be object such that
A58: n in NAT and
A59: m in NAT and
A60: nm=[n,m] by A56,ZFMISC_1:def 2;
reconsider Unn=Un.n as FamilySequence of T by A58,FUNCT_2:5,66;
UXk in Unn.m by A27,A54,A57,A58,A59,A60,A55;
then
A61: UXk in Union Unn by A59,PROB_1:12;
ex FS be FamilySequence of T st Un.n = FS & Union FS is open & Union
FS is Cover of T & Union FS is_finer_than FB.n & FS is sigma_discrete by A17
,A58;
then UXk9 is open by A61;
hence thesis by PRE_TOPC:def 2;
end;
then Union UX is Basis of T by A28,YELLOW_9:32;
then UX is Basis_sigma_discrete by A53,NAGATA_1:def 5;
hence thesis;
end;
::$N Bing metrization theorem
theorem
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
proof
let T;
now
assume that
A1: T is regular & T is T_1 and
A2: ex Bn be FamilySequence of T st Bn is Basis_sigma_discrete;
consider Bn be FamilySequence of T such that
A3: Bn is Basis_sigma_discrete by A2;
Bn is sigma_discrete by A3,NAGATA_1:def 5;
then
A4: Bn is sigma_locally_finite by NAGATA_1:12;
Union Bn is Basis of T by A3,NAGATA_1:def 5;
then Bn is Basis_sigma_locally_finite by A4,NAGATA_1:def 6;
hence T is metrizable by A1,Th19;
end;
hence thesis by Th21,NAGATA_1:15;
end;