x0; then
consider l be Element of NAT such that
A40: m = F.l by A21;
n<=l by A39,A40,SEQM_3:7; then
||. (f/*(s2*F)).l - f/.x0 .|| < p by A38; then
||. f/.((s2*F).l) - f/.x0 .|| < p
by A2,A34,FUNCT_2:186,XBOOLE_1:1; then
||. f/.(s2.m) - f/.x0 .|| < p by A40,FUNCT_2:21;
hence ||. (f/*s2).m - f/.x0 .|| < p by A2,FUNCT_2:186;
end;
end;
hence f/*s2 is convergent by NORMSP_1:def 9;
hence f/.x0=lim(f/*s2) by A36,NORMSP_1:def 11;
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 & abs(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: abs(x2-x1)~~~~ Lipschitzian 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 PartFunc of REAL,the carrier of S;
existence
proof
reconsider e = {} as PartFunc of REAL,the carrier of S by RELSET_1:25;
take e;
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 PartFunc of REAL,the carrier of S;
coherence
proof
consider r be real number such that
A1: 0~~~~ Lipschitzian PartFunc of REAL,the carrier of S;
coherence
proof
set X = dom f1, X1 = dom f2;
consider s such that
A8: 0~~~~ Lipschitzian 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*abs(x1-x2) by Def3;
per cases;
suppose A3: p=0;
now take s;
thus 0~~~~0; then
0 < abs p by COMPLEX1:133; then
A6:0 * s < abs(p) * s by A1,XREAL_1:70;
now take g = abs(p)*s;
A7: 0 <= abs p by COMPLEX1:132;
thus 0~~~~ Lipschitzian 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 8
.= f.x2 by A1,A2,FUNCT_1:def 16
.= f/.x2 by A2,PARTFUN1:def 8; then
||. f/.x1-f/.x2 .|| = 0 by NORMSP_1:10;
hence ||. f/.x1-f/.x2 .|| <= 1*abs(x1-x2) by COMPLEX1:132;
end;
hence thesis by Def3;
end;
end;
registration let S;
cluster Lipschitzian -> continuous 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 number such that
A1: 0~~