:: Lebesgue's Covering Lemma, Uniform Continuity and Segmentation of Arcs
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received November 13, 1997
:: Copyright (c) 1997-2016 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, REAL_1, SUBSET_1, XXREAL_0, CARD_1, ARYTM_3, RELAT_1,
XBOOLE_0, METRIC_1, FUNCT_1, FCONT_2, PARTFUN1, PRE_TOPC, PCOMPS_1,
ORDINAL2, RCOMP_1, ORDINAL1, STRUCT_0, TARSKI, SETFAM_1, FINSET_1,
ZFMISC_1, TOPMETR, BORSUK_1, EUCLID, FINSEQ_1, ORDINAL4, COMPLEX1,
ARYTM_1, XXREAL_1, VALUED_0, MEASURE5, NAT_1, INT_1, XXREAL_2, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, SETFAM_1, COMPLEX1, REAL_1, NAT_D, INT_1, NAT_1, RCOMP_1,
FUNCT_1, PARTFUN1, FINSEQ_1, RELSET_1, FUNCT_2, SEQM_3, STRUCT_0,
TOPMETR, PRE_TOPC, TOPS_2, COMPTS_1, EUCLID, FINSET_1, TBSP_1, METRIC_1,
PCOMPS_1;
constructors REAL_1, RCOMP_1, TOPS_2, COMPTS_1, TBSP_1, TOPMETR, GOBOARD1,
NAT_D, FUNCSDOM, PCOMPS_1, NUMBERS;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, NAT_1,
INT_1, FINSEQ_1, STRUCT_0, METRIC_1, PCOMPS_1, EUCLID, TOPMETR, BORSUK_2,
VALUED_0, FUNCT_2, BORSUK_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, ORDINAL1;
equalities XCMPLX_0;
expansions TARSKI;
theorems TARSKI, RCOMP_1, TOPMETR, TOPS_1, METRIC_1, FUNCT_1, FUNCT_2, TBSP_1,
NAT_1, FINSEQ_3, FINSEQ_1, ABSVALUE, PRE_TOPC, TOPS_2, FINSEQ_4,
GOBOARD6, PCOMPS_1, SETFAM_1, SUBSET_1, COMPTS_1, SEQ_4, HEINE, INT_1,
JORDAN2B, XBOOLE_0, XBOOLE_1, XREAL_0, FINSEQ_2, XCMPLX_1, FINSET_1,
XREAL_1, XXREAL_0, PARTFUN1, XXREAL_1, EUCLID, SEQM_3, ORDINAL1;
schemes FUNCT_2, DOMAIN_1, SUBSET_1, FINSEQ_1, NAT_1;
begin :: 1. Lebesgue's Covering Lemma
reserve x,y for set;
reserve s,s1,s2,s4,r,r1,r2 for Real;
reserve n,m,i,j for Element of NAT;
theorem Th1:
for r st r>0 ex n being Nat st n>0 & 1/n < r
proof
let r such that
A1: r>0;
A2: 1/r>0 by A1;
consider n being Nat such that
A3: 1/r < n by SEQ_4:3;
1/r*r {} & P9 is open by TOPMETR:14;
hence thesis by A1,TOPS_2:43;
end;
theorem Th3:
for N, M being non empty MetrSpace, f being Function of
TopSpaceMetr(N),TopSpaceMetr(M) holds (for r being Real,u being Element
of N,u1 being Element of M st r>0 & u1=f.u ex s being Real
st s>0 & for w being Element of N, w1 being Element of M st w1=f.w &
dist(u,w)~~0 & u1=f.u ex s be Real st s>0 & for w being
Element of N, w1 being Element of M st w1=f.w & dist(u,w)~~~~0 & P=Ball(u,r) holds f"P is open
proof
let r be Real,u be Element of M,P be Subset of
TopSpaceMetr(M);
reconsider P9=P as Subset of TopSpaceMetr(M);
assume that
r>0 and
A3: P=Ball(u,r);
for p being Point of N st p in f"P ex s being Real st s>0 &
Ball(p,s) c= f"P
proof
let p be Point of N;
assume p in f"P;
then
A4: f.p in Ball(u,r) by A3,FUNCT_1:def 7;
then reconsider wf=f.p as Element of M;
P9 is open by A3,TOPMETR:14;
then consider r1 being Real such that
A5: r1>0 and
A6: Ball(wf,r1) c= P by A3,A4,TOPMETR:15;
reconsider r1 as Real;
consider s be Real such that
A7: s>0 and
A8: for w being Element of N, w1 being Element of M st w1=f.w &
dist(p,w)~~~~0 & u1=f.u ex s st
s>0 & for w being Element of N, w1 being Element of M st w1=f.w & dist(u,w)~~~~0 & u1=f.u;
then f.u in P by GOBOARD6:1;
then
A3: u in f"P by A2,FUNCT_1:def 7;
f"P is open by A1,Th2;
then consider s1 be Real such that
A4: s1>0 and
A5: Ball(u,s1) c= f"P by A3,TOPMETR:15;
reconsider s1 as Real;
for w being Element of N, w1 being Element of M st w1=f.w & dist(u,w)0 & u1=g.u ex s be Real st s>0 & for w being Element
of N, w1 being Element of M st w1=g.w & dist(u,w)~~~~0 and
A4: u1=g.u;
consider s be Real such that
A5: 0~~~~0 & for w1,w2 being Element of N st dist(w1,w2)0 & for w1,w2 being Element of N st dist(w1,w2) {}
proof
let p be Element of NAT;
(f.p) in {x where x is Point of N : ex n st p<=n & x = f.n};
hence thesis;
end;
reconsider B0 as Subset of TopSpaceMetr(N) by A4,A10;
reconsider F as Subset-Family of TopSpaceMetr(N);
set G1 = clf F;
A13: Cl B0 in G1 by A11,PCOMPS_1:def 2;
G1 <> {} & for Gd being set st Gd <> {} & Gd c= G1 & Gd is finite
holds meet Gd <> {}
proof
thus G1<>{} by A13;
let H be set such that
A14: H <> {} and
A15: H c= G1 and
A16: H is finite;
reconsider H as Subset-Family of TM by A15,TOPS_2:2;
H is c=-linear
proof
let B,C be set;
assume that
A17: B in H and
A18: C in H;
reconsider B as Subset of TM by A17;
consider V being Subset of TM such that
A19: B = Cl V and
A20: V in F by A15,A17,PCOMPS_1:def 2;
consider p such that
A21: V = {x where x is Point of N : ex n st p<=n & x = f.n} by A9,A20;
reconsider C as Subset of TM by A18;
consider W being Subset of TM such that
A22: C = Cl W and
A23: W in F by A15,A18,PCOMPS_1:def 2;
consider q being Element of NAT such that
A24: W = {x where x is Point of N : ex n st q<=n & x = f.n} by A9,A23;
now
per cases;
case
A25: q<=p;
thus V c= W
proof
let y be object;
assume y in V;
then consider x being Point of N such that
A26: y = x and
A27: ex n st p<=n & x = f.n by A21;
consider n such that
A28: p<=n and
A29: x = f.n by A27;
q<=n by A25,A28,XXREAL_0:2;
hence thesis by A24,A26,A29;
end;
end;
case
A30: p<=q;
thus W c= V
proof
let y be object;
assume y in W;
then consider x being Point of N such that
A31: y = x and
A32: ex n st q<=n & x = f.n by A24;
consider n such that
A33: q<=n and
A34: x = f.n by A32;
p<=n by A30,A33,XXREAL_0:2;
hence thesis by A21,A31,A34;
end;
end;
end;
then B c= C or C c= B by A19,A22,PRE_TOPC:19;
hence thesis by XBOOLE_0:def 9;
end;
then consider m being set such that
A35: m in H and
A36: for C being set st C in H holds m c= C by A14,A16,FINSET_1:11;
A37: m c= meet H by A14,A36,SETFAM_1:5;
reconsider m as Subset of TM by A35;
consider A being Subset of TM such that
A38: m = Cl A and
A39: A in F by A15,A35,PCOMPS_1:def 2;
A <> {} by A9,A12,A39;
then m <> {} by A38,PRE_TOPC:18,XBOOLE_1:3;
hence thesis by A37;
end;
then G1 is closed & G1 is centered by FINSET_1:def 3,PCOMPS_1:11;
then meet G1 <> {} by A3,COMPTS_1:4;
then consider c being Point of TM such that
A40: c in meet G1 by SUBSET_1:4;
reconsider c as Point of N by A4;
consider Ge being Subset of TM such that
A41: c in Ge and
A42: Ge in G by A1,PCOMPS_1:3;
reconsider Ge as Subset of TM;
Ge is open by A2,A42,TOPS_2:def 1;
then consider r be Real such that
A43: r>0 and
A44: Ball(c,r) c= Ge by A41,TOPMETR:15;
reconsider r as Real;
consider n being Nat such that
A45: n>0 and
A46: 1/n < r/2 by A43,Th1,XREAL_1:215;
reconsider Q1=Ball(c,r/2) as Subset of TopSpaceMetr(N) by TOPMETR:12;
A47: Q1 is open by TOPMETR:14;
defpred Q[set] means ex n2 being Element of NAT st n<=n2 & $1 = f.n2;
reconsider B2 = {x where x is Point of TopSpaceMetr(N) : Q[x]} as Subset
of TopSpaceMetr(N) from DOMAIN_1:sch 7;
A48: n in NAT by ORDINAL1:def 12;
A49: the carrier of TopSpaceMetr(N) = the carrier of N by TOPMETR:12;
then B2 in F by A9,A48;
then Cl B2 in clf F by PCOMPS_1:def 2;
then
A50: c in Cl B2 by A40,SETFAM_1:def 1;
c in Q1 by A43,GOBOARD6:1,XREAL_1:215;
then B2 meets Q1 by A50,A47,TOPS_1:12;
then consider x being object such that
A51: x in B2 and
A52: x in Q1 by XBOOLE_0:3;
consider y being Point of N such that
A53: x=y and
A54: ex n2 being Element of NAT st n<=n2 & y=f.n2 by A49,A51;
A55: dist(c,y)=1/(n+1) by A45,NAT_1:11,XREAL_1:85;
then
A56: 1/(n+1) =1/(n2+1) by XREAL_1:118;
then dist(y,w2)<1/(n+1) by A59,XXREAL_0:2;
then dist(y,w2)r/2 by A43,XREAL_1:76;
then dist(c,y)0 and
A9: for u5 being Element of N, w5 being Element of M st w5=g.u5 &
dist(w0,u5)0 and
A12: for w1,w2 being Element of N st dist(w1,w2))=len f +1 & len (
<*x*>^f)=len f +1 & (f^<*x*>).(len f +1)=x & (<*x*>^f).1=x
proof
let x be set,f be FinSequence;
A1: len (<*x*>^f)=len <*x*> + len f by FINSEQ_1:22
.=len f+1 by FINSEQ_1:39;
1<=len <*x*> by FINSEQ_1:39;
then
A2: 1 in dom <*x*> by FINSEQ_3:25;
then
A3: (<*x*>^f).1=<*x*>.1 by FINSEQ_1:def 7
.=x by FINSEQ_1:def 8;
(f^<*x*>).(len f +1)=<*x*>.1 by A2,FINSEQ_1:def 7
.=x by FINSEQ_1:def 8;
hence thesis by A1,A3,FINSEQ_2:16;
end;
Lm5: for x being set,f being FinSequence st 1<=len f holds (f^<*x*>).1=f.1 & (
<*x*>^f).(len f +1)=f.len f
proof
let x be set,f be FinSequence;
assume
A1: 1<=len f;
then
A2: len f in dom f by FINSEQ_3:25;
A3: (<*x*>^f).(len f +1)=(<*x*>^f).(len <*x*>+len f) by FINSEQ_1:39
.=f.len f by A2,FINSEQ_1:def 7;
1 in dom f by A1,FINSEQ_3:25;
hence thesis by A3,FINSEQ_1:def 7;
end;
theorem Th11:
for r,s being Real holds |.r-s.|=|.s-r.|
proof
let r,s be Real;
per cases by XXREAL_0:1;
suppose
r>s;
then s-r<0 by XREAL_1:49;
then |.s-r.|=-(s-r) by ABSVALUE:def 1
.=r-s;
hence thesis;
end;
suppose
r=s;
hence thesis;
end;
suppose
r~~~~=0 by A4,XREAL_1:48;
then |.r2-r1.|<=s2-s1 by A5,ABSVALUE:def 1;
hence thesis by Th11;
end;
suppose
r1>r2;
then
A6: r1-r2>=0 by XREAL_1:48;
r1-r2<=s2-s1 by A2,XREAL_1:13;
hence thesis by A6,ABSVALUE:def 1;
end;
end;
definition
let IT be FinSequence of REAL;
attr IT is decreasing means
for n,m st n in dom IT & m in dom IT & n< m holds IT.n > IT.m;
end;
Lm7: for f being FinSequence of REAL st (for k being Nat st 1<=k &
kf/.(k+1)
holds f is decreasing
proof
let f be FinSequence of REAL;
assume
A1: for k being Nat st 1<=k & kf/.(k+1);
now
let i,j;
now
defpred P[Nat] means i+(1+$1)<=len f implies f/.i>f/.(i+(1+$1));
assume that
A2: i in dom f and
A3: j in dom f and
A4: if/.(i+(1+k));
now
1<=i+1 & i+1<=i+1+k by NAT_1:11;
then
A8: 1<=i+1+k by XXREAL_0:2;
A9: i+(1+(k+1)) =i+(1+k)+1;
1+k<1+(k+1) by NAT_1:13;
then
A10: i+(1+k)~~*f/.(i+(1+(k+1))) by A1,A8,A9;
hence f/.i>f/.(i+(1+(k+1))) by A7,A11,A10,XXREAL_0:2;
end;
hence thesis;
end;
i+1<=j by A4,NAT_1:13;
then j-'(i+1)=j-(i+1) by XREAL_1:233;
then
A12: i+(1+(j-'(i+1)))= j;
A13: f/.i=f.i by A2,PARTFUN1:def 6;
A14: j<=len f by A3,FINSEQ_3:25;
then if/.j by A14,A12;
hence f.i>f.j by A3,A13,PARTFUN1:def 6;
end;
hence i in dom f & j in dom f & if.j;
end;
hence thesis;
end;
theorem
for e being Real,
g being Function of I[01],TOP-REAL n, p1,p2 being
Element of TOP-REAL n st e>0 & g is continuous ex h being FinSequence of REAL
st h.1=0 & h.len h=1 & 5<=len h & rng h c=the carrier of I[01] & h is
increasing & for i being Nat,Q being Subset of I[01], W being Subset
of Euclid n st 1<=i & i0 and
A5: g is continuous;
A6: e/2>0 by A4,XREAL_1:215;
A7: the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
then reconsider h=g as Function of I[01], TopSpaceMetr Euclid n;
reconsider f=h as Function of Closed-Interval-MSpace(0,1),Euclid n by Lm3,
EUCLID:67;
A8: dom g=the carrier of I[01] by FUNCT_2:def 1;
h is continuous by A5,A7,PRE_TOPC:33;
then f is uniformly_continuous by Lm1,Th7,TOPMETR:20;
then consider s1 being Real such that
A9: 0) c= REAL
proof
let y be object;
A20: len (p^<*1*>)=len p + len <*1*> by FINSEQ_1:22
.=len p+1 by FINSEQ_1:40;
assume y in rng (p^<*1*>);
then consider x being object such that
A21: x in dom (p^<*1*>) and
A22: y=(p^<*1*>).x by FUNCT_1:def 3;
reconsider nx=x as Element of NAT by A21;
A23: dom (p^<*1*>)=Seg len (p^<*1*>) by FINSEQ_1:def 3;
then
A24: nx<=len (p^<*1*>) by A21,FINSEQ_1:1;
A25: 1<=nx by A21,A23,FINSEQ_1:1;
A26: 1<=nx by A21,A23,FINSEQ_1:1;
per cases;
suppose
nx=len p+1;
then nx=len p+1 by A24,A20,XXREAL_0:1;
then
A29: y=1 by A22,Lm4;
1 in REAL by XREAL_0:def 1;
hence thesis by A29;
end;
end;
then reconsider h1=p^<*1*> as FinSequence of REAL by FINSEQ_1:def 4;
A30: len h1=len p+len <*1*> by FINSEQ_1:22
.=len p+1 by FINSEQ_1:40;
A31: len p=j by A18,FINSEQ_1:def 3;
A32: s<>0 by A9,XXREAL_0:15;
then 2/s>=2/(1/2) by A11,XREAL_1:118,XXREAL_0:17;
then 4<=j by A12,XXREAL_0:2;
then
A33: 4+1<=len p+1 by A31,XREAL_1:6;
A34: s/2>0 by A11,A32,XREAL_1:215;
A35: for i being Nat,r1,r2 st 1<=i & i0 by A9,XXREAL_0:15;
then
A44: s/2*(2/s)=(2*s)/(2*s) & (2*s)/(2*s)=1 by XCMPLX_1:60,76;
then
A45: 1-s/2*(j-1)=s/2*(1+(2/s-[/ (2/s) \]));
A46: for r1 st r1=p.len p holds 1-r1<=s/2
by A42,A31,FINSEQ_1:1,A16,A18,A45;
A47: for i being Nat st 1<=i & i=len p;
then
A56: i=len p by A52,XXREAL_0:1;
A57: h1/.i=h1.i by A48,A49,FINSEQ_4:15
.=p.i by A48,A52,FINSEQ_1:64;
h1/.(i+1)=h1.(i+1) by A50,A51,FINSEQ_4:15
.=1 by A56,Lm4;
hence thesis by A46,A56,A57;
end;
end;
hence thesis;
end;
[/ (2/s) \]<2/s+1 by INT_1:def 7;
then [/ (2/s) \]-1<2/s+1-1 by XREAL_1:9;
then
A58: s/2*(j-1)*~~=len p;
then
A73: i=len p by A68,XXREAL_0:1;
A74: h1/.i=h1.i by A65,A66,FINSEQ_4:15
.=p.i by A65,A68,FINSEQ_1:64;
h1/.(i+1)=h1.(i+1) by A69,A67,FINSEQ_4:15
.=1 by A73,Lm4;
hence thesis by A59,A65,A68,A74;
end;
end;
A75: e/2{} by A78,XXREAL_1:1;
A81: for x,y being Point of Euclid n st x in W & y in W holds dist(x,y)<= e/2
proof
let x,y be Point of Euclid n;
assume that
A82: x in W and
A83: y in W;
consider x3 being object such that
A84: x3 in dom g and
A85: x3 in Q and
A86: x=g.x3 by A79,A82,FUNCT_1:def 6;
reconsider x3 as Element of Closed-Interval-MSpace(0,1) by A84,Lm2,
TOPMETR:12;
reconsider r3=x3 as Real by A78,A85;
A87: h1/.(i+1)-h1/.i<=s/2 by A47,A77;
consider y3 being object such that
A88: y3 in dom g and
A89: y3 in Q and
A90: y=g.y3 by A79,A83,FUNCT_1:def 6;
reconsider y3 as Element of Closed-Interval-MSpace(0,1) by A88,Lm2,
TOPMETR:12;
reconsider s3=y3 as Real by A78,A89;
A91: f.x3=(f/.x3) & f.y3=(f/.y3);
|.r3-s3.|<=h1/.(i+1)-h1/.i by A78,A85,A89,Th12;
then |.r3-s3.|<=s/2 by A87,XXREAL_0:2;
then
A92: dist(x3,y3)<=s/2 by HEINE:1;
s/2~~~~=1-1 by XREAL_1:9;
nx<=len p by A97,FINSEQ_1:1;
then ry<1 by A59,A98;
then y in {rs where rs is Real:0<=rs & rs<=1} by A11,A95,A96,A99;
hence thesis by RCOMP_1:def 1;
end;
rng <*1*> ={1} by FINSEQ_1:38;
then rng h1 =rng p \/ {1} by FINSEQ_1:31;
then
A100: rng h1 c=[.0,1.] \/ {1} by A93,XBOOLE_1:13;
h1.len h1=1 by A30,Lm4;
hence thesis by A30,A33,A43,A2,A100,A3,A64,A76,Lm7;
end;
theorem
for e being Real,g being Function of I[01], (TOP-REAL n), p1,p2 being
Element of TOP-REAL n st e>0 & g is continuous ex h being FinSequence of REAL
st h.1=1 & h.len h=0 & 5<=len h & rng h c= the carrier of I[01] & h is
decreasing & for i being Nat,Q being Subset of I[01], W being Subset
of Euclid n st 1<=i & i0 and
A4: g is continuous;
A5: e/2>0 by A3,XREAL_1:215;
h is continuous by A4,A2,PRE_TOPC:33;
then f is uniformly_continuous by Lm1,Th7,TOPMETR:20;
then consider s1 being Real such that
A6: 0) c= REAL
proof
let y be object;
A17: len (p^<*0 qua Real*>)=len p + len <*0 qua Real*> by FINSEQ_1:22
.=len p+1 by FINSEQ_1:40;
assume y in rng (p^<*0 qua Real*>);
then consider x being object such that
A18: x in dom (p^<*0 qua Real*>) and
A19: y=(p^<*0 qua Real*>).x by FUNCT_1:def 3;
reconsider nx=x as Element of NAT by A18;
A20: dom (p^<*0 qua Real*>)=Seg len (p^<*0 qua Real*>) by FINSEQ_1:def 3;
then
A21: nx<=len (p^<*0 qua Real*>) by A18,FINSEQ_1:1;
A22: 1<=nx by A18,A20,FINSEQ_1:1;
A23: 1<=nx by A18,A20,FINSEQ_1:1;
now
per cases;
case
nx=len p+1;
then nx=len p+1 by A21,A17,XXREAL_0:1;
then y=In(0,REAL) by A19,Lm4;
hence thesis;
end;
end;
hence thesis;
end;
then reconsider h1=p^<*0 qua Real*> as FinSequence of REAL by FINSEQ_1:def 4;
A26: len h1=len p+len <*0 qua Real*> by FINSEQ_1:22
.=len p+1 by FINSEQ_1:40;
A27: len p=j by A15,FINSEQ_1:def 3;
A28: s<>0 by A6,XXREAL_0:15;
then 2/s>=2/(1/2) by A8,XREAL_1:118,XXREAL_0:17;
then 4<=j by A9,XXREAL_0:2;
then
A29: 4+1<=len p+1 by A27,XREAL_1:6;
A30: s/2>0 by A8,A28,XREAL_1:215;
A31: for i being Nat,r1,r2 st 1<=i & ir2 & r1-r2=s/2
proof
let i be Nat,r1,r2;
assume that
A32: 1<=i & ir2 by A35,A36,XREAL_1:15;
thus thesis by A35,A36;
end;
0~~~~0 by A6,XXREAL_0:15;
then
A39: s/2*(2/s)=(2*s)/(2*s) & (2*s)/(2*s)=1 by XCMPLX_1:60,76;
then
A40: 1-s/2*(j-1)=s/2*(1+(2/s-[/ (2/s) \]));
A41: for r1 st r1=p.len p holds r1-0<=s/2
by A37,A27,FINSEQ_1:1,A15,A13,A40;
A42: for i being Nat st 1<=i & i=len p;
then
A51: i=len p by A47,XXREAL_0:1;
A52: h1/.i=h1.i by A43,A44,FINSEQ_4:15
.=p.i by A43,A47,FINSEQ_1:64;
h1/.(i+1)=h1.(i+1) by A45,A46,FINSEQ_4:15
.=0 by A51,Lm4;
hence thesis by A41,A51,A52;
end;
end;
hence thesis;
end;
[/ (2/s) \]<2/s+1 by INT_1:def 7;
then [/ (2/s) \]-1<2/s+1-1 by XREAL_1:9;
then
A53: s/2*(j-1)~~~~1-1 by XREAL_1:10;
i in Seg j by A16,A55,A56,FINSEQ_1:1;
hence thesis by A15,A57,A58;
end;
A59: for i being Nat st 1<=i & ih1/.(i+1)
proof
let i be Nat;
assume that
A60: 1<=i and
A61: i=len p;
then
A68: i=len p by A63,XXREAL_0:1;
A69: h1/.i=h1.i by A60,A61,FINSEQ_4:15
.=p.i by A60,A63,FINSEQ_1:64;
h1/.(i+1)=h1.(i+1) by A64,A62,FINSEQ_4:15
.=0 by A68,Lm4;
hence thesis by A54,A60,A63,A69;
end;
end;
hence thesis;
end;
A70: e/2h1/.(i+1) by A59,A72;
then
A75: Q<>{} by A73,XXREAL_1:1;
A76: for x,y being Point of Euclid n st x in W & y in W holds dist(x,y)<= e/2
proof
let x,y be Point of Euclid n;
assume that
A77: x in W and
A78: y in W;
consider x3 being object such that
A79: x3 in dom g and
A80: x3 in Q and
A81: x=g.x3 by A74,A77,FUNCT_1:def 6;
reconsider x3 as Element of Closed-Interval-MSpace(0,1) by A79,Lm2,
TOPMETR:12;
reconsider r3=x3 as Real by A73,A80;
A82: x=(f/.x3) by A81;
consider y3 being object such that
A83: y3 in dom g and
A84: y3 in Q and
A85: y=g.y3 by A74,A78,FUNCT_1:def 6;
reconsider y3 as Element of Closed-Interval-MSpace(0,1) by A83,Lm2,
TOPMETR:12;
reconsider s3=y3 as Real by A73,A84;
A86: h1/.i-h1/.(i+1)<=s/2 by A42,A72;
|.r3-s3.|<=h1/.i-h1/.(i+1) by A73,A80,A84,Th12;
then
A87: |.r3-s3.|<=s/2 by A86,XXREAL_0:2;
dist(x3,y3)=|.r3-s3.| & s/2~~~~=1-1 by XREAL_1:9;
then
A97: 1-s/2*(nx-1)<=1-0 by A8,XREAL_1:6;
nx<=len p by A95,FINSEQ_1:1;
then 0 ={0} by FINSEQ_1:38;
then rng h1 =rng p \/ {0} by FINSEQ_1:31;
then
A98: rng h1 c=[.0,1.] \/ {0} by A91,XBOOLE_1:13;
h1.len h1=0 by A26,Lm4;
hence thesis by A26,A29,A38,A89,A98,A90,A59,A71,Lm8;
end;
~~