x0; then
consider l be Nat such that
A39: m = F.l by A20;
A40: l in NAT by ORDINAL1:def 12;
n<=l by A37,A39,SEQM_3:1; then
||. (f/*(s2*F)).l - f/.x0 .|| < p by A36; then
||. f/.((s2*F).l) - f/.x0 .|| < p
by A2,A32,FUNCT_2:109,XBOOLE_1:1,A40; then
||. f/.(s2.m) - f/.x0 .|| < p by A39,FUNCT_2:15,A40;
hence ||. (f/*s2).m - f/.x0 .|| < p by A2,FUNCT_2:109,A38;
end;
end;
hence f/*s2 is convergent by NORMSP_1:def 6;
hence f/.x0=lim(f/*s2) by A34,NORMSP_1:def 7;
end;
end;
theorem Th8:
f is_continuous_in x0 iff
x0 in dom f &
for r st 0 < r ex s
st 0 < s & for x1 st x1 in dom f & |.x1-x0.| < s
holds ||. f/.x1 - f/.x0 .|| < r
proof
thus f is_continuous_in x0 implies
x0 in dom f
& for r st 0~~0 by A9;
let x2 such that
x2 in REAL and
A11: |.x2-x1.|~~~~ Lipschitzian for PartFunc of REAL,the carrier of S;
coherence
proof
let f be PartFunc of REAL,the carrier of S;
assume A1: f is empty;
take 1;
thus thesis by A1;
end;
end;
registration let S;
cluster empty for PartFunc of REAL,the carrier of S;
existence
proof
take the empty PartFunc of REAL,the carrier of S;
thus thesis;
end;
end;
registration
let S;
let f be Lipschitzian PartFunc of REAL,the carrier of S, X be set;
cluster f|X -> Lipschitzian for PartFunc of REAL,the carrier of S;
coherence
proof
consider r be Real such that
A1: 0~~~~ Lipschitzian for PartFunc of REAL,the carrier of S;
coherence
proof
set X = dom f1, X1 = dom f2;
consider s such that
A8: 0~~~~ Lipschitzian for PartFunc of REAL, the carrier of S;
coherence
proof
consider s such that
A1: 0 < s and
A2: for x1,x2 st x1 in dom f & x2 in dom f
holds ||.f/.x1-f/.x2.|| <= s*|.x1-x2.| by Def3;
per cases;
suppose A3: p=0;
now take s;
thus 0~~~~0; then
0 < |.p.| by COMPLEX1:47; then
A6:0 * s < |.p.| * s by A1,XREAL_1:68;
now take g = |.p.|*s;
A7: 0 <= |.p.| by COMPLEX1:46;
thus 0~~~~ Lipschitzian for PartFunc of REAL, the carrier of S;
coherence
proof
let f be PartFunc of REAL, the carrier of S such that
A1: f is constant;
now let x1,x2;
assume A2: x1 in dom f & x2 in dom f; then
f/.x1 = f.x1 by PARTFUN1:def 6
.= f.x2 by A1,A2,FUNCT_1:def 10
.= f/.x2 by A2,PARTFUN1:def 6; then
||. f/.x1-f/.x2 .|| = 0 by NORMSP_1:6;
hence ||. f/.x1-f/.x2 .|| <= 1*|.x1-x2.| by COMPLEX1:46;
end;
hence thesis;
end;
end;
registration let S;
cluster Lipschitzian -> continuous for PartFunc of REAL, the carrier of S;
coherence
proof
let f be PartFunc of REAL, the carrier of S;
set X = dom f;
assume f is Lipschitzian; then
consider r be Real such that
A1: 0~~