:: Lebesgue's Covering Lemma, Uniform Continuity and Segmentation of Arcs
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received November 13, 1997
:: Copyright (c) 1997-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, 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<n*r by A1,A3,XREAL_1:68;
then 1<n*r by A1,XCMPLX_1:87;
then 1/n<r by A3,A2,XREAL_1:83;
hence thesis by A3,A2;
end;
definition
let X,Y be non empty MetrStruct,f be Function of X,Y;
attr f is uniformly_continuous means
for r st 0<r ex s st 0<s & for
u1,u2 being Element of X st dist(u1,u2) < s holds dist(f/.u1,f/.u2) < r;
end;
theorem Th2:
for X being non empty TopSpace, M being non empty MetrSpace, f
being Function of X,TopSpaceMetr(M) st f is continuous
for r being Real,u
being Element of M,P being Subset of TopSpaceMetr(M) st P=Ball(u
,r) holds f"P is open
proof
let X be non empty TopSpace, M be non empty MetrSpace, f be Function of X,
TopSpaceMetr(M);
assume
A1: f is continuous;
let r be Real,u be Element of M,P be Subset of TopSpaceMetr
(M);
reconsider P9=P as Subset of TopSpaceMetr(M);
assume P=Ball(u,r);
then [#]TopSpaceMetr M <> {} & 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)<s holds dist(u1,w1)<r) implies f is continuous
proof
let N,M be non empty MetrSpace,f be Function of TopSpaceMetr(N),
TopSpaceMetr(M);
dom f = the carrier of TopSpaceMetr(N) by FUNCT_2:def 1;
then
A1: dom f=the carrier of N by TOPMETR:12;
now
assume
A2: for r being Real,u being Element of N,u1
being Element of M st r>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)<s holds dist(u1,w1)<r
;
for r being Real,u being Element of M,P being
Subset of TopSpaceMetr(M) st r>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)<s holds dist(wf,w1)<r1 by A2,A5;
reconsider s as Real;
Ball(p,s) c= f"P
proof
let x be object;
assume
A9: x in Ball(p,s);
then reconsider wx=x as Element of N;
f.wx in rng f by A1,FUNCT_1:def 3;
then reconsider wfx=f.wx as Element of M by TOPMETR:12;
dist (p,wx)<s by A9,METRIC_1:11;
then dist(wf,wfx)<r1 by A8;
then wfx in Ball(wf,r1) by METRIC_1:11;
hence thesis by A1,A6,FUNCT_1:def 7;
end;
hence thesis by A7;
end;
hence thesis by TOPMETR:15;
end;
hence f is continuous by JORDAN2B:16;
end;
hence thesis;
end;
theorem Th4:
for N, M being non empty MetrSpace, f being Function of
TopSpaceMetr(N),TopSpaceMetr(M) st f is continuous
for r being Real,u
being Element of N,u1 being Element of M st r>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)<s
holds dist(u1,w1)<r
proof
let N, M be non empty MetrSpace, f be Function of TopSpaceMetr(N),
TopSpaceMetr(M);
assume
A1: f is continuous;
let r be Real,u be Element of N,u1 be Element of M;
reconsider P=Ball(u1,r) as Subset of TopSpaceMetr(M) by TOPMETR:12;
A2: the carrier of N=the carrier of TopSpaceMetr(N) & dom f=the carrier of
TopSpaceMetr(N) by FUNCT_2:def 1,TOPMETR:12;
assume r>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)<s1
holds dist(u1,w1)<r
proof
let w be Element of N, w1 be Element of M;
assume that
A6: w1=f.w and
A7: dist(u,w)<s1;
w in Ball(u,s1) by A7,METRIC_1:11;
then f.w in P by A5,FUNCT_1:def 7;
hence thesis by A6,METRIC_1:11;
end;
hence thesis by A4;
end;
theorem
for N,M being non empty MetrSpace, f being Function of N,M, g being
Function of TopSpaceMetr(N),TopSpaceMetr(M) st f=g & f is uniformly_continuous
holds g is continuous
proof
let N,M be non empty MetrSpace, f be Function of N,M, g be Function of
TopSpaceMetr(N),TopSpaceMetr(M);
assume that
A1: f=g and
A2: f is uniformly_continuous;
for r being Real,u being Element of N,u1 being
Element of M st r>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)<s holds dist(u1,w1)<r
proof
let r be Real, u be Element of N,u1 be Element of M;
reconsider r9=r as Real;
assume that
A3: r>0 and
A4: u1=g.u;
consider s be Real such that
A5: 0<s and
A6: for wu1,wu2 being Element of N st dist(wu1,wu2) < s holds dist((f
/. wu1),(f/.wu2)) < r by A2,A3;
for w being Element of N, w1 being Element of M st w1=g.w & dist(u,w)<
s holds dist(u1,w1)<r
proof
let w be Element of N, w1 be Element of M;
assume that
A7: w1=g.w and
A8: dist(u,w)<s;
A9: u1=f/.u by A1,A4;
w1=f/.w by A1,A7;
hence thesis by A6,A8,A9;
end;
hence thesis by A5;
end;
hence thesis by Th3;
end;
reserve p for Element of NAT;
::$N Lebesgue's Covering Lemma
theorem Th6:
for N being non empty MetrSpace, G being Subset-Family of
TopSpaceMetr(N) st G is Cover of TopSpaceMetr(N) & G is open & TopSpaceMetr(N)
is compact ex r st r>0 & for w1,w2 being Element of N st dist(w1,w2)<r holds ex
Ga being Subset of TopSpaceMetr(N) st w1 in Ga & w2 in Ga & Ga in G
proof
let N be non empty MetrSpace, G be Subset-Family of TopSpaceMetr(N);
assume that
A1: G is Cover of TopSpaceMetr(N) and
A2: G is open and
A3: TopSpaceMetr(N) is compact;
now
set TM = TopSpaceMetr(N);
defpred P[object,object] means
(for n being Element of NAT,w1 being Element of N
st n=$1 & w1=$2 ex w2 being Element of N st dist(w1,w2)<1/(n+1) & for Ga being
Subset of TopSpaceMetr(N) holds not(w1 in Ga & w2 in Ga & Ga in G ) );
A4: TM = TopStruct (# the carrier of N,Family_open_set(N) #) by PCOMPS_1:def 5;
assume
A5: not ex r st r>0 & for w1,w2 being Element of N st dist(w1,w2)<r
holds ex Ga being Subset of TopSpaceMetr(N) st w1 in Ga & w2 in Ga & Ga in G;
A6: for e being object st e in NAT
ex u being object st u in the carrier of N & P[e,u]
proof
let e be object;
assume e in NAT;
then reconsider m=e as Element of NAT;
set r=1/(m+1);
consider w1,w2 being Element of N such that
A7: dist(w1,w2)<r & for Ga being Subset of TopSpaceMetr(N) holds not
(w1 in Ga & w2 in Ga & Ga in G) by A5;
for n being Element of NAT,w4 being Element of N st n=e & w4=w1 ex
w5 being Element of N st dist(w4,w5)<1/(n+1) & for Ga being Subset of
TopSpaceMetr(N) holds not(w4 in Ga & w5 in Ga & Ga in G ) by A7;
hence thesis;
end;
ex f being sequence of the carrier of N st for e being object st e
in NAT holds P[e,f.e] from FUNCT_2:sch 1(A6);
then consider f being sequence of the carrier of N such that
A8: for e being object st e in NAT holds for n being Element of NAT,w1
being Element of N st n=e & w1=f.e ex w2 being Element of N st dist(w1,w2)<1/(n
+1) & for Ga being Subset of TopSpaceMetr(N) holds not(w1 in Ga & w2 in Ga & Ga
in G );
defpred P[Subset of TopSpaceMetr(N)] means ex p st $1 = {x where x is
Point of N : ex n st p<=n & x = f.n};
consider F being Subset-Family of TopSpaceMetr(N) such that
A9: for B being Subset of TopSpaceMetr(N) holds B in F iff P[B] from
SUBSET_1:sch 3;
defpred P[set] means ex n st 0<=n & $1 = f.n;
set B0 = {x where x is Point of N : P[x]};
A10: B0 is Subset of N from DOMAIN_1:sch 7;
then
A11: B0 in F by A4,A9;
A12: for p holds {x where x is Point of N : ex n st p<=n & x = f.n} <> {}
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)<r/2 by A52,A53,METRIC_1:11;
1/n>=1/(n+1) by A45,NAT_1:11,XREAL_1:85;
then
A56: 1/(n+1) <r/2 by A46,XXREAL_0:2;
consider n2 being Element of NAT such that
A57: n<=n2 and
A58: y=f.n2 by A54;
consider w2 being Element of N such that
A59: dist(y,w2)<1/(n2+1) and
A60: for Ga being Subset of TopSpaceMetr(N) holds not(y in Ga & w2 in
Ga & Ga in G ) by A8,A58;
n+1<=n2+1 by A57,XREAL_1:7;
then 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 A56,XXREAL_0:2;
then
A61: r/2+dist(y,w2)<r/2+r/2 by XREAL_1:6;
r/1>r/2 by A43,XREAL_1:76;
then dist(c,y)<r by A55,XXREAL_0:2;
then
A62: y in Ball(c,r) by METRIC_1:11;
dist(c,w2)<=dist(c,y)+dist(y,w2) & dist(c,y)+dist(y,w2)<r/2+dist(y,w2
) by A55,METRIC_1:4,XREAL_1:6;
then dist(c,w2)<r/2+dist(y,w2) by XXREAL_0:2;
then dist(c,w2)<r/2+r/2 by A61,XXREAL_0:2;
then w2 in Ball(c,r) by METRIC_1:11;
hence contradiction by A42,A44,A62,A60;
end;
hence thesis;
end;
begin :: 2. Uniformity of Continuous Functions on Compact Spaces
theorem Th7:
for N,M being non empty MetrSpace,f being Function of N,M, g
being Function of TopSpaceMetr(N),TopSpaceMetr(M) st g=f & TopSpaceMetr(N) is
compact & g is continuous holds f is uniformly_continuous
proof
let N,M be non empty MetrSpace,f be Function of N,M, g be Function of
TopSpaceMetr(N),TopSpaceMetr(M);
assume that
A1: g=f and
A2: TopSpaceMetr(N) is compact and
A3: g is continuous;
for r st 0<r ex s st 0<s & for u1,u2 being Element of N st dist(u1,u2) <
s holds dist((f/.u1),(f/.u2)) < r
proof
let r;
set G={P where P is Subset of TopSpaceMetr(N): ex w being Element of N,s
st P=Ball(w,s) & (for w1 being Element of N,w2,w3 being Element of M st w2=f.w
& w3=f.w1 & dist(w,w1)<s holds dist(w2,w3)<r/2)};
A4: the carrier of TopSpaceMetr(N)=the carrier of N by TOPMETR:12;
G c= bool the carrier of N
proof
let x be object;
assume x in G;
then ex P being Subset of TopSpaceMetr(N) st x=P & ex w being Element of
N,s st P=Ball(w,s) & for w1 being Element of N,w2,w3 being Element of M st w2=f
.w & w3=f.w1 & dist(w,w1)<s holds dist(w2,w3) < r/2;
hence thesis;
end;
then reconsider G1=G as Subset-Family of TopSpaceMetr(N) by TOPMETR:12;
for P3 being Subset of TopSpaceMetr(N) holds P3 in G1 implies P3 is open
proof
let P3 be Subset of TopSpaceMetr(N);
assume P3 in G1;
then
ex P being Subset of TopSpaceMetr(N) st P3=P & ex w being Element of
N,s st P=Ball(w,s) & for w1 being Element of N,w2,w3 being Element of M st w2=f
.w & w3=f.w1 & dist(w,w1)<s holds dist(w2,w3)<r/2;
hence thesis by TOPMETR:14;
end;
then
A5: G1 is open by TOPS_2:def 1;
assume 0<r;
then
A6: 0<r/2 by XREAL_1:215;
A7: the carrier of N c= union G1
proof
let x be object;
assume x in the carrier of N;
then reconsider w0=x as Element of N;
g.w0=(f/.w0) by A1;
then reconsider w4=g.w0 as Element of M;
consider s4 such that
A8: s4>0 and
A9: for u5 being Element of N, w5 being Element of M st w5=g.u5 &
dist(w0,u5)<s4 holds dist(w4,w5)<r/2 by A3,A6,Th4;
reconsider P2=Ball(w0,s4) as Subset of TopSpaceMetr(N) by TOPMETR:12;
for w1 being Element of N,w2,w3 being Element of M st w2=f.w0 & w3=
f.w1 & dist(w0,w1)<s4 holds dist(w2,w3)<r/2 by A1,A9;
then
ex w being Element of N,s st P2=Ball(w,s) & for w1 being Element of
N,w2,w3 being Element of M st w2=f.w & w3=f.w1 & dist(w,w1)<s holds dist(w2,w3)
<r/2;
then
A10: Ball(w0,s4) in G1;
x in Ball(w0,s4) by A8,GOBOARD6:1;
hence thesis by A10,TARSKI:def 4;
end;
the carrier of TopSpaceMetr(N)=the carrier of N by TOPMETR:12;
then the carrier of N=union G1 by A7,XBOOLE_0:def 10;
then G1 is Cover of TopSpaceMetr(N) by A4,SETFAM_1:45;
then consider s1 such that
A11: s1>0 and
A12: for w1,w2 being Element of N st dist(w1,w2)<s1 holds ex Ga being
Subset of TopSpaceMetr(N) st w1 in Ga & w2 in Ga & Ga in G1 by A2,A5,Th6;
for u1,u2 being Element of N st dist(u1,u2) < s1 holds dist((f/.u1),(
f/.u2)) < r
proof
let u1,u2 be Element of N;
assume dist(u1,u2) < s1;
then consider Ga being Subset of TopSpaceMetr(N) such that
A13: u1 in Ga and
A14: u2 in Ga and
A15: Ga in G1 by A12;
consider P being Subset of TopSpaceMetr(N) such that
A16: Ga=P and
A17: ex w being Element of N,s2 st P=Ball(w,s2) & for w1 being
Element of N,w2,w3 being Element of M st w2=f.w & w3=f.w1 & dist(w,w1)<s2 holds
dist(w2,w3)< r/2 by A15;
consider w being Element of N,s2 such that
A18: P=Ball(w,s2) and
A19: for w1 being Element of N,w2,w3 being Element of M st w2=f.w &
w3= f.w1 & dist(w,w1)<s2 holds dist(w2,w3)< r/2 by A17;
dist(w,u2)<s2 by A14,A16,A18,METRIC_1:11;
then
A20: dist((f/.w),(f/.u2))<r/2 by A19;
dist(w,u1)<s2 by A13,A16,A18,METRIC_1:11;
then dist((f/.w),(f/.u1))<r/2 by A19;
then
dist((f/.u1),(f/.u2)) <=dist((f/.u1),(f/.w))+dist((f/.w),(f/.u2)) &
dist((f /.w),(f/.u1))+dist((f/.w),(f/.u2)) <r/2+r/2 by A20,METRIC_1:4
,XREAL_1:8;
hence thesis by XXREAL_0:2;
end;
hence thesis by A11;
end;
hence thesis;
end;
Lm1: Closed-Interval-TSpace(0,1)=TopSpaceMetr(Closed-Interval-MSpace(0,1)) by
TOPMETR:def 7;
Lm2: I[01]=TopSpaceMetr(Closed-Interval-MSpace(0,1)) by TOPMETR:20,def 7;
Lm3: the carrier of I[01]=the carrier of Closed-Interval-MSpace(0,1) by Lm1,
TOPMETR:12,20;
theorem
for g being Function of I[01],TOP-REAL n, f being Function of
Closed-Interval-MSpace(0,1),Euclid n st g is continuous & f=g holds f is
uniformly_continuous
proof
let g be Function of I[01],TOP-REAL n, f being Function of
Closed-Interval-MSpace(0,1),Euclid n such that
A1: g is continuous and
A2: f=g;
A3: 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;
h is continuous by A1,A3,PRE_TOPC:33;
hence f is uniformly_continuous by A2,Lm1,Th7,TOPMETR:20;
end;
theorem
for P being Subset of TOP-REAL n, Q being non empty Subset of Euclid n
, g being Function of I[01],(TOP-REAL n)|P, f being Function of
Closed-Interval-MSpace(0,1),((Euclid n)|Q) st P=Q & g is continuous & f=g holds
f is uniformly_continuous
proof
let P be Subset of TOP-REAL n, Q be non empty Subset of Euclid n, g be
Function of I[01],(TOP-REAL n)|P, f be Function of Closed-Interval-MSpace(0,1),
((Euclid n)|Q);
assume that
A1: P=Q and
A2: g is continuous & f=g;
(TOP-REAL n)|P = TopSpaceMetr((Euclid n)|Q) by A1,EUCLID:63;
hence thesis by A2,Lm1,Th7,TOPMETR:20;
end;
begin :: 3. Segmentation of Arcs
theorem
for g being Function of I[01],TOP-REAL n holds g is Function of
Closed-Interval-MSpace(0,1),Euclid n by Lm3,EUCLID:67;
Lm4: for x being set,f being FinSequence holds len (f^<*x*>)=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;
(f^<*x*>).(len f +1)=<*x*>.1 by A2,FINSEQ_1:def 7
.=x;
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<s;
then r-s<0 by XREAL_1:49;
then |.r-s.|=-(r-s) by ABSVALUE:def 1
.=s-r;
hence thesis;
end;
end;
Lm6: for r,s1,s2 holds r in [.s1,s2.] iff s1<=r & r<=s2
proof
let r,s1,s2;
A1: now
assume r in [.s1,s2.];
then r in {r1:s1<=r1 & r1<=s2} by RCOMP_1:def 1;
then ex r1 st r1=r & s1<=r1 & r1<=s2;
hence s1<=r & r<=s2;
end;
now
assume s1<=r & r<=s2;
then r in {r1:s1<=r1 & r1<=s2};
hence r in [.s1,s2.] by RCOMP_1:def 1;
end;
hence thesis by A1;
end;
theorem Th12:
for r1,r2,s1,s2 st r1 in [.s1,s2.] & r2 in [.s1,s2.] holds |. r1-r2.|<=s2-s1
proof
let r1,r2,s1,s2;
assume
A1: r1 in [.s1,s2.] & r2 in [.s1,s2.];
then
A2: r1<=s2 & s1<=r2 by Lm6;
A3: s1<=r1 & r2<=s2 by A1,Lm6;
per cases;
suppose
A4: r1<=r2;
A5: r2-r1<=s2-s1 by A3,XREAL_1:13;
r2-r1>=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 &
k<len f holds f/.k<f/.(k+1)) holds f is increasing
proof
let f be FinSequence of REAL;
assume
A1: for k being Nat st 1<=k & k<len f holds f/.k<f/.(k+1);
now
let i,j be Nat;
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: i<j;
A5: 1<=i by A2,FINSEQ_3:25;
A6: for k being Nat st P[k] holds P[(k+1)]
proof
let k be Nat;
assume
A7: i+(1+k)<=len f implies f/.i<f/.(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)<i+(1+(k+1)) by XREAL_1:6;
assume
A11: i+(1+(k+1))<=len f;
then i+(1+k)<len f by A10,XXREAL_0:2;
then f/.(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 i<len f by A4,XXREAL_0:2;
then
A15: P[0] by A1,A5;
for k being Nat holds P[k] from NAT_1:sch 2(A15,A6);
then f/.i<f/.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 & i<j implies f.i<f.j;
end;
hence thesis by SEQM_3:def 1;
end;
Lm8: for f being FinSequence of REAL st
for k being Nat st 1<=k <len f holds f/.k>f/.(k+1)
holds f is decreasing
proof
let f be FinSequence of REAL;
assume
A1: for k being Nat st 1<=k & k<len f holds f/.k>f/.(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: i<j;
A5: 1<=i by A2,FINSEQ_3:25;
A6: for k being Nat st P[k] holds P[(k+1)]
proof
let k be Nat;
assume
A7: i+(1+k)<=len f implies f/.i>f/.(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)<i+(1+(k+1)) by XREAL_1:6;
assume
A11: i+(1+(k+1))<=len f;
then i+(1+k)<len f by A10,XXREAL_0:2;
then f/.(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 i<len f by A4,XXREAL_0:2;
then
A15: P[0] by A1,A5;
for k being Nat holds P[k] from NAT_1:sch 2(A15,A6);
then f/.i>f/.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 & i<j implies f.i>f.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 & i<len h & Q=[.h/.i,h/.(i+1).] & W=g.:(Q) holds diameter(W
)<e
proof
1 in {r where r is Real:0<=r & r<=1};
then
A1: 1 in [.0,1.] by RCOMP_1:def 1;
{1} c= [.0,1.]
by A1,TARSKI:def 1;
then
A2: [.0,1.] \/ {1} =[.0,1.] by XBOOLE_1:12;
Closed-Interval-TSpace(0,1) =TopSpaceMetr(Closed-Interval-MSpace(0,1))
by TOPMETR:def 7;
then
A3: the carrier of I[01] =the carrier of Closed-Interval-MSpace(0,1) by
TOPMETR:12,20
.= [.0,1.] by TOPMETR:10;
let e be Real,g be Function of I[01],TOP-REAL n, p1,p2 be Element of
TOP-REAL n;
assume that
A4: e>0 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<s1 and
A10: for u1,u2 being Element of (Closed-Interval-MSpace(0,1)) st dist(u1
,u2) < s1 holds dist((f/.u1),(f/.u2)) < e/2 by A6;
set s=min(s1,1/2);
defpred P[Nat,object] means $2=s/2*($1-1);
A11: 0<=s by A9,XXREAL_0:20;
then reconsider j= [/ (2/s) \] as Element of NAT by INT_1:53;
A12: 2/s<=j by INT_1:def 7;
A13: s<=s1 by XXREAL_0:17;
A14: for u1,u2 being Element of (Closed-Interval-MSpace(0,1)) st dist(u1,u2)
< s holds dist((f/.u1),(f/.u2)) < e/2
proof
let u1,u2 be Element of (Closed-Interval-MSpace(0,1));
assume dist(u1,u2) < s;
then dist(u1,u2) < s1 by A13,XXREAL_0:2;
hence thesis by A10;
end;
A15: 2/s<=[/ (2/s) \] by INT_1:def 7;
then 2/s-j<=0 by XREAL_1:47;
then 1+(2/s-j)<=1+0 by XREAL_1:6;
then
A16: s/2*(1+(2/s-j))<=s/2*1 by A11,XREAL_1:64;
A17: for k being Nat st k in Seg j ex x being object st P[k,x];
consider p being FinSequence such that
A18: dom p = Seg j & for k being Nat st k in Seg j holds P[k,p.k] from
FINSEQ_1:sch 1(A17);
A19: Seg len p=Seg j by A18,FINSEQ_1:def 3;
rng (p^<*1*>) 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
A27: nx<=len p by NAT_1:13;
then nx in Seg j by A19,A25,FINSEQ_1:1;
then
A28: p.nx=s/2*(nx-1) by A18;
y=p.nx by A22,A26,A27,FINSEQ_1:64;
hence thesis by A28,XREAL_0:def 1;
end;
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 & i<len p & r1=p.i & r2=p.(i+1
) holds r1<r2 & r2-r1=s/2
proof
let i be Nat,r1,r2;
assume that
A36: 1<=i & i<len p and
A37: r1=p.i and
A38: r2=p.(i+1);
1<i+1 & i+1<=len p by A36,NAT_1:13;
then (i+1) in Seg j by A19,FINSEQ_1:1;
then
A39: r2=s/2*(i+1-1) by A18,A38;
i<i+1 by NAT_1:13;
then
A40: i-1<i+1-1 by XREAL_1:9;
A41: i in Seg j by A19,A36,FINSEQ_1:1;
then r1=s/2*(i-1) by A18,A37;
hence r1<r2 by A34,A39,A40,XREAL_1:68;
r2-r1=s/2*(i)-s/2*(i-1) by A18,A37,A41,A39
.=s/2;
hence thesis;
end;
0<s by A9,XXREAL_0:15;
then 0<j by A15,XREAL_1:139;
then
A42: 0+1<=j by NAT_1:13;
then 1 in Seg j by FINSEQ_1:1;
then p.1=s/2*(1-1) by A18
.=0;
then
A43: h1.1=0 by A42,A31,Lm5;
2*s<>0 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 h1 holds h1/.(i+1)-h1/.i<=s /2
proof
let i be Nat;
assume that
A48: 1<=i and
A49: i<len h1;
A50: i+1<=len h1 by A49,NAT_1:13;
A51: 1<i+1 by A48,NAT_1:13;
A52: i<=len p by A30,A49,NAT_1:13;
now
per cases;
case
A53: i<len p;
then i+1<=len p by NAT_1:13;
then
A54: h1.(i+1)=p.(i+1) by A51,FINSEQ_1:64;
A55: h1.i=p.i by A48,A53,FINSEQ_1:64;
h1.i=h1/.i & h1.(i+1)=h1/.(i+1) by A48,A49,A50,A51,FINSEQ_4:15;
hence thesis by A35,A48,A53,A55,A54;
end;
case
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)<s/2*(2/s) by A34,XREAL_1:68;
A59: for i being Nat,r1 st 1<=i & i<=len p & r1=p.i holds r1<1
proof
let i be Nat,r1;
assume that
A60: 1<=i and
A61: i<=len p and
A62: r1=p.i;
i-1<=j-1 by A31,A61,XREAL_1:9;
then
A63: (s/2)*(i-1)<=(s/2)*(j-1) by A11,XREAL_1:64;
i in Seg j by A19,A60,A61,FINSEQ_1:1;
then r1=s/2*(i-1) by A18,A62;
hence thesis by A58,A44,A63,XXREAL_0:2;
end;
A64: for i being Nat st 1<=i & i<len h1 holds h1/.i<h1/.(i+1)
proof
let i be Nat;
assume that
A65: 1<=i and
A66: i<len h1;
A67: 1<i+1 by A65,NAT_1:13;
A68: i<=len p by A30,A66,NAT_1:13;
A69: i+1<=len h1 by A66,NAT_1:13;
per cases;
suppose
A70: i<len p;
then i+1<=len p by NAT_1:13;
then
A71: h1.(i+1)=p.(i+1) by A67,FINSEQ_1:64;
A72: h1.i=p.i by A65,A70,FINSEQ_1:64;
h1.i=h1/.i & h1.(i+1)=h1/.(i+1) by A65,A66,A69,A67,FINSEQ_4:15;
hence thesis by A35,A65,A70,A72,A71;
end;
suppose
i>=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<e by A4,XREAL_1:216;
A76: for i being Nat,Q being Subset of I[01], W being Subset of
Euclid n st 1<=i & i<len h1 & Q=[.h1/.i,h1/.(i+1).] & W=g.:(Q) holds diameter(W
)<e
proof
let i be Nat,Q be Subset of I[01], W be Subset of Euclid n;
assume that
A77: 1<=i & i<len h1 and
A78: Q=[.h1/.i,h1/.(i+1).] and
A79: W=g.:(Q);
h1/.i<h1/.(i+1) by A64,A77;
then
A80: Q<>{} 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<s by A11,A32,XREAL_1:216;
then dist(x3,y3)<s by A92,XXREAL_0:2;
hence thesis by A14,A86,A90,A91;
end;
then W is bounded by A6,TBSP_1:def 7;
then diameter(W)<=e/2 by A8,A79,A80,A81,TBSP_1:def 8;
hence thesis by A75,XXREAL_0:2;
end;
A93: rng p c=[.0,1.]
proof
let y be object;
assume y in rng p;
then consider x being object such that
A94: x in dom p and
A95: y=p.x by FUNCT_1:def 3;
reconsider nx=x as Element of NAT by A94;
A96: p.nx=s/2*(nx-1) by A18,A94;
then reconsider ry=p.nx as Real;
A97: x in Seg len p by A94,FINSEQ_1:def 3;
then
A98: 1<=nx by FINSEQ_1:1;
then
A99: nx-1>=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 & i<len h & Q=[.h/.(i+1),h/.i.] & W=g.:(Q) holds diameter(W
)<e
proof
let e be Real,g be Function of I[01], (TOP-REAL n), p1,p2 be Element of
TOP-REAL n;
A1: dom g=the carrier of I[01] by FUNCT_2:def 1;
A2: 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=g as Function of Closed-Interval-MSpace(0,1),(Euclid n) by Lm3,
EUCLID:67;
assume that
A3: e>0 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<s1 and
A7: for u1,u2 being Element of (Closed-Interval-MSpace(0,1)) st dist(u1
,u2) < s1 holds dist((f/.u1),(f/.u2)) < e/2 by A5;
set s=min(s1,1/2);
defpred P[Nat,object] means $2=1-s/2*($1-1);
A8: 0<=s by A6,XXREAL_0:20;
then reconsider j = [/ (2/s) \] as Element of NAT by INT_1:53;
A9: 2/s<=j by INT_1:def 7;
A10: s<=s1 by XXREAL_0:17;
A11: for u1,u2 being Element of (Closed-Interval-MSpace(0,1)) st dist(u1,u2)
< s holds dist((f/.u1),(f/.u2)) < e/2
proof
let u1,u2 be Element of (Closed-Interval-MSpace(0,1));
assume dist(u1,u2) < s;
then dist(u1,u2) < s1 by A10,XXREAL_0:2;
hence thesis by A7;
end;
A12: 2/s<=[/ (2/s) \] by INT_1:def 7;
then 2/s-j<=0 by XREAL_1:47;
then 1+(2/s-j)<=1+0 by XREAL_1:6;
then
A13: s/2*(1+(2/s-j))<=s/2*1 by A8,XREAL_1:64;
A14: for k being Nat st k in Seg j ex x being object st P[k,x];
consider p being FinSequence such that
A15: dom p = Seg j & for k being Nat st k in Seg j holds P[k,p.k] from
FINSEQ_1:sch 1(A14);
A16: Seg len p=Seg j by A15,FINSEQ_1:def 3;
rng (p^<*0 qua Real*>) 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
A24: nx<=len p by NAT_1:13;
then nx in Seg j by A16,A22,FINSEQ_1:1;
then
A25: p.nx=1-s/2*(nx-1) by A15;
y=p.nx by A19,A23,A24,FINSEQ_1:64;
hence thesis by A25,XREAL_0:def 1;
end;
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 & i<len p & r1=p.i & r2=p.(i+1
) holds r1>r2 & r1-r2=s/2
proof
let i be Nat,r1,r2;
assume that
A32: 1<=i & i<len p and
A33: r1=p.i and
A34: r2=p.(i+1);
i in Seg j by A16,A32,FINSEQ_1:1;
then
A35: r1=1-s/2*(i-1) by A15,A33;
1<i+1 & i+1<=len p by A32,NAT_1:13;
then (i+1) in Seg j by A16,FINSEQ_1:1;
then
A36: r2=1-s/2*(i+1-1) by A15,A34;
i<i+1 by NAT_1:13;
then i-1<i+1-1 by XREAL_1:9;
then (s/2)*(i-1)<(s/2)*(i+1-1) by A30,XREAL_1:68;
hence r1>r2 by A35,A36,XREAL_1:15;
thus thesis by A35,A36;
end;
0<s by A6,XXREAL_0:15;
then 0<j by A12,XREAL_1:139;
then
A37: 0+1<=j by NAT_1:13;
then 1 in Seg j by FINSEQ_1:1;
then p.1=1-s/2*(1-1) by A15
.=1;
then
A38: h1.1=1 by A37,A27,Lm5;
2*s<>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 h1 holds h1/.i-h1/.(i+1)<=s /2
proof
let i be Nat;
assume that
A43: 1<=i and
A44: i<len h1;
A45: i+1<=len h1 by A44,NAT_1:13;
A46: 1<i+1 by A43,NAT_1:13;
A47: i<=len p by A26,A44,NAT_1:13;
now
per cases;
case
A48: i<len p;
then i+1<=len p by NAT_1:13;
then
A49: h1.(i+1)=p.(i+1) by A46,FINSEQ_1:64;
A50: h1.i=p.i by A43,A48,FINSEQ_1:64;
h1.i=h1/.i & h1.(i+1)=h1/.(i+1) by A43,A44,A45,A46,FINSEQ_4:15;
hence thesis by A31,A43,A48,A50,A49;
end;
case
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)<s/2*(2/s) by A30,XREAL_1:68;
A54: for i being Nat,r1 st 1<=i & i<=len p & r1=p.i holds 0<r1
proof
let i be Nat,r1;
assume that
A55: 1<=i and
A56: i<=len p and
A57: r1=p.i;
i-1<=j-1 by A27,A56,XREAL_1:9;
then (s/2)*(i-1)<=(s/2)*(j-1) by A8,XREAL_1:64;
then (s/2)*(i-1)<1 by A53,A39,XXREAL_0:2;
then
A58: 1-(s/2)*(i-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 & i<len h1 holds h1/.i>h1/.(i+1)
proof
let i be Nat;
assume that
A60: 1<=i and
A61: i<len h1;
A62: 1<i+1 by A60,NAT_1:13;
A63: i<=len p by A26,A61,NAT_1:13;
A64: i+1<=len h1 by A61,NAT_1:13;
now
per cases;
case
A65: i<len p;
then i+1<=len p by NAT_1:13;
then
A66: h1.(i+1)=p.(i+1) by A62,FINSEQ_1:64;
A67: h1.i=p.i by A60,A65,FINSEQ_1:64;
h1.i=h1/.i & h1.(i+1)=h1/.(i+1) by A60,A61,A64,A62,FINSEQ_4:15;
hence thesis by A31,A60,A65,A67,A66;
end;
case
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/2<e by A3,XREAL_1:216;
A71: for i being Nat,Q being Subset of I[01], W being Subset of
Euclid n st 1<=i & i<len h1 & Q=[.h1/.(i+1),h1/.i.] & W=g.:(Q) holds diameter(W
)<e
proof
let i be Nat,Q be Subset of I[01], W be Subset of Euclid n;
assume that
A72: 1<=i & i<len h1 and
A73: Q=[.h1/.(i+1),h1/.i.] and
A74: W=g.:(Q);
h1/.i>h1/.(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<s by A8,A28,HEINE:1,XREAL_1:216;
then f.y3=(f/.y3) & dist(x3,y3)<s by A87,XXREAL_0:2;
hence thesis by A11,A85,A82;
end;
then W is bounded by A5,TBSP_1:def 7;
then diameter(W)<=e/2 by A1,A74,A75,A76,TBSP_1:def 8;
hence thesis by A70,XXREAL_0:2;
end;
0 in {r where r is Real:0<=r & r<=1};
then
A88: 0 in [.0,1.] by RCOMP_1:def 1;
{0} c= [.0,1.]
by A88,TARSKI:def 1;
then
A89: [.0,1.] \/ {0} =[.0,1.] by XBOOLE_1:12;
Closed-Interval-TSpace(0,1) =TopSpaceMetr(Closed-Interval-MSpace(0,1))
by TOPMETR:def 7;
then
A90: the carrier of I[01] =the carrier of Closed-Interval-MSpace(0,1) by
TOPMETR:12,20
.= [.0 qua Real,1.] by TOPMETR:10;
A91: rng p c=[.0,1.]
proof
let y be object;
assume y in rng p;
then consider x being object such that
A92: x in dom p and
A93: y=p.x by FUNCT_1:def 3;
reconsider nx=x as Element of NAT by A92;
A94: p.nx=1-s/2*(nx-1) by A15,A92;
then reconsider ry=p.nx as Real;
A95: x in Seg len p by A92,FINSEQ_1:def 3;
then
A96: 1<=nx by FINSEQ_1:1;
then nx-1>=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<ry by A54,A96;
then y in {rs where rs is Real:0<=rs & rs<=1} by A93,A94,A97;
hence thesis by RCOMP_1:def 1;
end;
rng <*0 qua Real*> ={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;