:: More on Continuous Functions on Normed Linear Spaces
:: by Hiroyuki Okazaki , Noboru Endou and Yasunari Shidama
::
:: Received August 17, 2010
:: Copyright (c) 2010-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, SEQ_1, PARTFUN1, RELAT_1, TARSKI, SEQ_2,
ORDINAL2, FUNCT_2, FUNCT_1, XBOOLE_0, XXREAL_0, NAT_1, ARYTM_3, CARD_1,
COMPLEX1, ARYTM_1, REAL_1, RCOMP_1, XXREAL_1, VALUED_1, ZFMISC_1,
VALUED_0, FCONT_1, NORMSP_1, STRUCT_0, SUPINF_2, PRE_TOPC;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1,
PARTFUN1, FUNCT_2, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, NAT_1,
VALUED_0, COMPLEX1, ZFMISC_1, SEQ_1, SEQ_2, RCOMP_1, FCONT_1, STRUCT_0,
PRE_TOPC, RLVECT_1, VFUNCT_1, NORMSP_0, NORMSP_1, NFCONT_1;
constructors REAL_1, COMPLEX1, MEMBERED, SEQ_2, RCOMP_1, RELSET_1, FCONT_1,
NFCONT_1, VFUNCT_1, COMSEQ_2, NUMBERS;
registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED,
VALUED_0, FUNCT_2, RELAT_1, FUNCT_1, STRUCT_0, VFUNCT_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions FCONT_1;
equalities RELAT_1, RLVECT_1;
expansions FCONT_1;
theorems TARSKI, ZFMISC_1, NAT_1, FUNCT_1, FUNCT_2, SEQ_2, SEQM_3, SEQ_4,
PARTFUN1, XREAL_0, PARTFUN2, RCOMP_1, RELAT_1, RELSET_1, XBOOLE_0,
XBOOLE_1, XCMPLX_0, XCMPLX_1, XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1,
MEMBERED, VALUED_0, NFCONT_1, NORMSP_0, NORMSP_1, RLVECT_1, LOPBAN_3,
VFUNCT_1, LOPBAN_1, BHSP_1, NUMBERS;
schemes NAT_1, RECDEF_1, FUNCT_2;
begin :: Preliminaries
reserve n,m,k for Nat;
reserve x,X,X1 for set;
reserve r,p for Real;
reserve s,g,x0,x1,x2 for Real;
reserve S,T for RealNormSpace;
reserve f,f1,f2 for PartFunc of REAL,the carrier of S;
reserve s1,s2 for Real_Sequence;
reserve Y for Subset of REAL;
theorem Th1:
for seq be Real_Sequence, h be PartFunc of REAL, the carrier of S
st rng seq c= dom h holds seq.n in dom h
proof
let seq be Real_Sequence;
let h be PartFunc of REAL,the carrier of S;
n in NAT by ORDINAL1:def 12; then
A1:n in dom seq by FUNCT_2:def 1;
assume rng seq c= dom h; then
n in dom ((h qua Function)*seq) by A1,RELAT_1:27;
hence thesis by FUNCT_1:11;
end;
theorem Th2:
for h1,h2 be PartFunc of REAL,the carrier of S
for seq be Real_Sequence
st rng seq c= dom h1 /\ dom h2
holds (h1+h2)/*seq = h1/*seq + h2/*seq & (h1-h2)/*seq = h1/*seq - h2/*seq
proof
let h1,h2 be PartFunc of REAL,the carrier of S;
let seq be Real_Sequence;
A1:dom h1 /\ dom h2 c= dom h1 & dom h1 /\ dom h2 c= dom h2
by XBOOLE_1:17;
assume A2: rng seq c= dom h1 /\ dom h2;
now let n be Nat;
A3: n in NAT by ORDINAL1:def 12;
A4: h1/.(seq.n) = (h1/*seq).n & h2/.(seq.n) = (h2/*seq).n
by A1,A2,FUNCT_2:109,XBOOLE_1:1,A3;
A5: rng seq c= dom (h1 + h2) by A2,VFUNCT_1:def 1; then
A6: seq.n in dom (h1 + h2) by Th1;
thus ((h1+h2)/*seq).n = (h1+h2)/.(seq.n) by A5,FUNCT_2:109,A3
.= (h1/*seq).n + (h2/*seq).n by A4,A6,VFUNCT_1:def 1;
end;
hence (h1+h2)/*seq = h1/*seq+h2/*seq by NORMSP_1:def 2;
now let n be Nat;
A7: n in NAT by ORDINAL1:def 12;
A8: h1/.(seq.n) = (h1/*seq).n & h2/.(seq.n) = (h2/*seq).n
by A1,A2,FUNCT_2:109,XBOOLE_1:1,A7;
A9: rng seq c= dom (h1 - h2) by A2,VFUNCT_1:def 2; then
A10: seq.n in dom (h1 - h2) by Th1;
thus ((h1-h2)/*seq).n = (h1-h2)/.(seq.n) by A9,FUNCT_2:109,A7
.= (h1/*seq).n - (h2/*seq).n by A8,A10,VFUNCT_1:def 2;
end;
hence thesis by NORMSP_1:def 3;
end;
theorem
for h be sequence of S,r be Real holds r(#)h = r*h
proof
let h be sequence of S;
let r be Real;
A1: dom h = NAT by FUNCT_2:def 1; then
A2:dom (r(#)h) = NAT by VFUNCT_1:def 4;
now let n;
A3: n in NAT by ORDINAL1:def 12;
then (r(#)h).n = (r(#)h)/.n by A2,PARTFUN1:def 6; then
(r(#)h).n = r * (h/.n) by A2,VFUNCT_1:def 4,A3;
hence (r(#)h).n = r * (h.n) by A3,PARTFUN1:def 6,A1;
end;
hence thesis by NORMSP_1:def 5;
end;
theorem Th4:
for h be PartFunc of REAL,the carrier of S,
seq be Real_Sequence, r be Real
st rng seq c= dom h holds (r(#)h)/*seq = r*(h/*seq)
proof
let h be PartFunc of REAL,the carrier of S,
seq be Real_Sequence, r be Real;
assume A1: rng seq c= dom h; then
A2:rng seq c= dom (r(#)h) by VFUNCT_1:def 4;
now let n;
A3: n in NAT by ORDINAL1:def 12;
A4: seq.n in dom (r(#)h) by A2,Th1;
thus ((r(#)h)/*seq).n = (r(#)h)/.(seq.n) by A2,FUNCT_2:109,A3
.= r * (h/.(seq.n)) by A4,VFUNCT_1:def 4
.= r * (h/*seq).n by A1,FUNCT_2:109,A3;
end;
hence thesis by NORMSP_1:def 5;
end;
theorem Th5:
for h be PartFunc of REAL,the carrier of S,
seq be Real_Sequence
st rng seq c= dom h
holds ||.h/*seq .|| = ||.h.||/*seq
& -(h/*seq) = (-h)/*seq
proof
let h be PartFunc of REAL,the carrier of S,
seq be Real_Sequence;
assume A1: rng seq c= dom h; then
A2:rng seq c= dom ||.h.|| by NORMSP_0:def 3;
now
let n be Element of NAT;
seq.n in rng seq by FUNCT_2:4; then
seq.n in dom h by A1; then
A3: seq.n in dom ||.h.|| by NORMSP_0:def 3;
thus ||.h/*seq.||.n = ||.(h/*seq).n.|| by NORMSP_0:def 4
.= ||.h/.(seq.n).|| by A1,FUNCT_2:109
.= ||.h.||.(seq.n) by A3,NORMSP_0:def 3
.= ||.h.||/.(seq.n) by A3,PARTFUN1:def 6
.= (||.h.||/*seq).n by A2,FUNCT_2:109;
end;
hence ||.h/*seq.|| = (||.h.||)/*seq by FUNCT_2:63;
now let n be Element of NAT;
thus (-(h/*seq)).n = - ((h/*seq).n) by BHSP_1:44
.= (-1) * (h/*seq).n by RLVECT_1:16
.= ((-1)*(h/*seq)).n by NORMSP_1:def 5
.= (((-1)(#)h)/*seq).n by A1,Th4
.= ((-h)/*seq).n by VFUNCT_1:23;
end;
hence -(h/*seq) = (-h)/*seq by FUNCT_2:63;
end;
begin :: Continuous Real Functions into Normed Linear Spaces
definition
let S,f,x0;
pred f is_continuous_in x0 means
x0 in dom f
& for s1 st rng s1 c= dom f & s1 is convergent & lim s1 = x0
holds f/*s1 is convergent & f/.x0 = lim (f/*s1);
end;
theorem Th6:
x0 in X & f is_continuous_in x0 implies f|X is_continuous_in x0
proof
assume that
A1: x0 in X and
A2: f is_continuous_in x0;
A3:x0 in dom f by A2;
A4:dom(f|X) = X /\ dom f by RELAT_1:61;
hence
A5: x0 in dom (f|X) by A1,A3,XBOOLE_0:def 4;
let s1 such that
A6: rng s1 c= dom(f|X) and
A7: s1 is convergent & lim s1 = x0;
A8:rng s1 c= dom f by A6,A4,XBOOLE_1:18;
A9:(f|X)/*s1 = f/*s1 by A6,FUNCT_2:117;
hence (f|X)/*s1 is convergent by A2,A7,A8;
x0 in REAL by XREAL_0:def 1;
hence (f|X)/.x0 = f/.x0 by A5,PARTFUN2:15
.= lim ((f|X)/*s1) by A2,A7,A8,A9;
end;
theorem
f is_continuous_in x0 iff
x0 in dom f
& for s1 st rng s1 c= dom f & s1 is convergent
& lim s1 = x0 & (for n holds s1.n<>x0)
holds f/*s1 is convergent & f/.x0 = lim(f/*s1)
proof
thus f is_continuous_in x0 implies
x0 in dom f
& for s1 st rng s1 c= dom f & s1 is convergent & lim s1=x0
& (for n holds s1.n<>x0) holds f/*s1 is convergent
& f/.x0=lim(f/*s1);
assume
A1: x0 in dom f & for s1 st
rng s1 c=dom f & s1 is convergent & lim s1=x0 & (for n holds s1.n<>x0)
holds f/*s1 is convergent & f/.x0=lim(f/*s1);
thus x0 in dom f by A1;
let s2 such that
A2: rng s2 c=dom f and
A3: s2 is convergent & lim s2=x0;
per cases;
suppose ex n st for m st n<=m holds s2.m=x0; then
consider N be Nat such that
A4: for m st N<=m holds s2.m=x0;
A5: f/*(s2^\N)=(f/*s2)^\N by A2,VALUED_0:27;
A6: now let p be Real such that
A7: p>0;
reconsider n=0 as Nat;
take n;
let m such that n<=m;
A8: s2.(m+N) = x0 by A4,NAT_1:12;
A9: m in NAT by ORDINAL1:def 12;
rng (s2^\N) c= rng s2 by VALUED_0:21; then
||.(f/*(s2^\N)).m - f/.x0 .||
= ||. f/.((s2^\N).m) - f/.x0 .|| by A2,FUNCT_2:109,XBOOLE_1:1,A9
.= ||. f/.x0 - f/.x0 .|| by A8,NAT_1:def 3
.= 0 by NORMSP_1:6;
hence ||. (f/*(s2^\N)).m - f/.x0 .|| < p by A7;
end; then
A10:f/*(s2^\N) is convergent by NORMSP_1:def 6; then
f/.x0=lim((f/*s2)^\N) by A6,A5,NORMSP_1:def 7;
hence thesis by A10,A5,LOPBAN_3:10,11;
end;
suppose
A11:for n ex m st n<=m & s2.m<>x0;
defpred P[Nat,set,set] means
for n,m st $2 = n & $3 = m
holds n < m & s2.m <> x0
& (for k st n < k & s2.k <> x0 holds m <= k);
defpred P[set] means s2.$1 <> x0;
ex m1 be Nat st 0<=m1 & s2.m1<>x0 by A11; then
A12:ex m be Nat st P[m];
consider M be Nat such that
A13: P[M] & for n be Nat st P[n] holds M<=n from NAT_1:sch 5(A12);
reconsider M9 = M as Element of NAT by ORDINAL1:def 12;
A14:now let n;
consider m such that
A15: n+1 <= m & s2.m <> x0 by A11;
take m;
thus n < m & s2.m <> x0 by A15,NAT_1:13;
end;
A16:for n being Nat, x being Element of NAT
ex y be Element of NAT st P[n,x,y]
proof
let n be Nat, x be Element of NAT;
defpred P[Nat] means x < $1 & s2.$1 <> x0;
ex m st P[m] by A14; then
A17: ex m be Nat st P[m];
consider l be Nat such that
A18: P[l] & for k be Nat st P[k] holds l<=k from NAT_1:sch 5(A17);
take l;
l in NAT by ORDINAL1:def 12;
hence thesis by A18;
end;
consider F be sequence of NAT such that
A19: F.0 = M9 & for n being Nat holds P[n,F.n,F.(n+1)]
from RECDEF_1:sch 2(A16);
dom F = NAT & rng F c= REAL by FUNCT_2:def 1,XBOOLE_1:1,NUMBERS:19; then
reconsider F as Real_Sequence by RELSET_1:4;
for n holds F.n < F.(n+1) by A19;
then reconsider F as increasing sequence of NAT by SEQM_3:def 6;
A20:for n st s2.n<>x0 ex m st F.m=n
proof
defpred P[set] means s2.$1<>x0 & for m holds F.m<>$1;
assume ex n st P[n]; then
A21: ex n be Nat st P[n];
consider M1 be Nat such that
A22: P[M1] & for n be Nat st P[n] holds M1<=n from NAT_1:sch 5(A21);
reconsider M1 as Nat;
defpred P[Nat] means $1<M1 & s2.$1<>x0 & ex m st F.m=$1;
A23: ex n being Nat st P[n]
proof
take M;
M<=M1 & M <> M1 by A13,A19,A22;
hence M<M1 by XXREAL_0:1;
thus s2.M<>x0 by A13;
take 0;
thus thesis by A19;
end;
A24: for n being Nat st P[n] holds n<=M1;
consider MX be Nat such that
A25: P[MX] & for n being Nat st P[n] holds n<=MX from NAT_1:sch 6(A24,A23);
consider m such that
A26: F.m = MX by A25;
A27: MX < F.(m+1) & s2.(F.(m+1)) <> x0 by A19,A26;
F.(m+1) <> M1 & F.(m+1) <= M1 by A19,A22,A25,A26; then
F.(m+1) < M1 by XXREAL_0:1;
hence contradiction by A25,A27;
end;
A28:for n holds (s2*F).n<>x0
proof
defpred P[Nat] means (s2*F).$1<>x0;
A29: for k st P[k] holds P[k+1]
proof
let k such that (s2*F).k<>x0;
reconsider k as Element of NAT by ORDINAL1:def 12;
F.k in NAT & F.(k+1) in NAT; then
s2.(F.(k+1))<>x0 by A19;
hence thesis by FUNCT_2:15;
end;
A30: P[0] by A13,A19,FUNCT_2:15;
thus for n holds P[n] from NAT_1:sch 2(A30,A29);
end;
A31:s2*F is convergent & lim (s2*F)=x0 by A3,SEQ_4:16,17;
A32:rng (s2*F) c= rng s2 by VALUED_0:21; then
rng (s2*F) c= dom f by A2,XBOOLE_1:1; then
A33:f/*(s2*F) is convergent & f/.x0 = lim(f/*(s2*F)) by A1,A28,A31;
A34:now let p be Real;
assume A35: 0<p; then
consider n such that
A36: for m st n<=m holds ||.(f/*(s2*F)).m - f/.x0 .||<p
by A33,NORMSP_1:def 7;
reconsider k=F.n as Nat;
take k;
let m such that A37: k <= m;
A38: m in NAT by ORDINAL1:def 12;
per cases;
suppose s2.m=x0; then
||.(f/*s2).m - f/.x0.|| = ||. f/.x0-f/.x0 .|| by A2,FUNCT_2:109,A38
.= 0 by NORMSP_1:6;
hence ||.(f/*s2).m - f/.x0 .||<p by A35;
end;
suppose s2.m<>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<r ex s st 0<s & for x1 st x1 in dom f & |.x1-x0.| < s
holds ||. f/.x1 - f/.x0 .|| < r
proof
assume A1: f is_continuous_in x0;
hence x0 in dom f;
given r such that
A2: 0 < r and
A3: for s holds not 0 < s
or ex x1 st x1 in dom f & |.x1-x0.| < s & not ||. f/.x1 - f/.x0 .|| < r;
defpred P[Nat,Real] means
$2 in dom f & |.$2-x0.| < 1/($1+1) & not ||. f/.$2 - f/.x0 .||<r;
A4: for n being Element of NAT ex p being Element of REAL st P[n,p]
proof
let n be Element of NAT;
0 < (n+1)"; then
0 < 1/(n+1) by XCMPLX_1:215; then
consider x1 such that
A5: x1 in dom f & |.x1-x0.| < 1/(n+1) & not ||. f/.x1 - f/.x0 .|| < r
by A3;
take x1;
thus thesis by A5;
end;
consider s1 such that
A6: for n being Element of NAT holds P[n,s1.n] from FUNCT_2:sch 3(A4);
now let x be object;
assume x in rng s1; then
ex n being Element of NAT st x=s1.n by FUNCT_2:113;
hence x in dom f by A6;
end; then
A7: rng s1 c= dom f by TARSKI:def 3;
A8: now let s be Real;
assume A9: 0<s;
consider n such that
A10: s"<n by SEQ_4:3;
s"+(0 qua Nat) <n+1 by A10,XREAL_1:8; then
1/(n+1) < 1/s" by A9,XREAL_1:76; then
A11: 1/(n+1) < s by XCMPLX_1:216;
take k=n;
let m;
A12: m in NAT by ORDINAL1:def 12;
assume k <= m; then
k+1 <= m+1 by XREAL_1:6; then
1/(m+1) <= 1/(k+1) by XREAL_1:118; then
1/(m+1) < s by A11,XXREAL_0:2;
hence |.s1.m-x0.| < s by A6,XXREAL_0:2,A12;
end; then
A13:s1 is convergent by SEQ_2:def 6; then
lim s1=x0 by A8,SEQ_2:def 7; then
f/*s1 is convergent & f/.x0=lim(f/*s1) by A1,A7,A13; then
consider n such that
A14: for m st n<=m holds ||.(f/*s1).m-f/.x0 .||<r by A2,NORMSP_1:def 7;
A15: n in NAT by ORDINAL1:def 12;
||. (f/*s1).n - f/.x0 .||<r by A14; then
||. f/.(s1.n) - f/.x0 .|| < r by A7,FUNCT_2:109,A15;
hence contradiction by A6,A15;
end;
assume
A16: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;
now let s1 such that
A17: rng s1 c= dom f and
A18: s1 is convergent & lim s1 = x0;
A19:now let p be Real;
assume 0 < p; then
consider s such that
A20: 0 < s and
A21: for x1 st x1 in dom f & |.x1-x0.|<s holds ||. f/.x1 - f/.x0 .||<p by A16;
consider n such that
A22: for m st n<=m holds |.s1.m-x0.|<s by A18,A20,SEQ_2:def 7;
take k=n;
let m;
A23: m in NAT by ORDINAL1:def 12;
assume k<=m; then
s1.m in rng s1 & |.s1.m-x0.|<s by A22,VALUED_0:28; then
||.f/.(s1.m)-f/.x0 .||<p by A17,A21;
hence ||.(f/*s1).m - f/.x0 .||<p by A17,FUNCT_2:109,A23;
end; then
f/*s1 is convergent by NORMSP_1:def 6;
hence f/*s1 is convergent & f/.x0 = lim (f/*s1) by A19,NORMSP_1:def 7;
end;
hence thesis by A16;
end;
theorem Th9:
for S,f,x0 holds f is_continuous_in x0 iff
x0 in dom f
& for N1 being Neighbourhood of f/.x0
ex N being Neighbourhood of x0
st for x1 st x1 in dom f & x1 in N holds f/.x1 in N1
proof
let S,f,x0;
thus f is_continuous_in x0 implies
x0 in dom f & for N1 being Neighbourhood of f/.x0
ex N being Neighbourhood of x0 st
for x1 st x1 in dom f & x1 in N holds f/.x1 in N1
proof
assume A1: f is_continuous_in x0;
hence x0 in dom f;
let N01 be Neighbourhood of f/.x0;
consider r such that
A2: 0<r and
A3: { p where p is Point of S : ||. p - f/.x0 .|| < r } c= N01
by NFCONT_1:def 1;
set N1={ p where p is Point of S : ||. p - f/.x0 .|| < r };
consider s such that
A4: 0<s and
A5: for x1 st x1 in dom f & |.x1-x0.| < s holds ||. f/.x1 - f/.x0 .||<r
by A1,A2,Th8;
reconsider N = ].x0-s,x0+s.[ as Neighbourhood of x0 by A4,RCOMP_1:def 6;
take N;
let x1;
assume that
A6: x1 in dom f and
A7: x1 in N;
|.x1-x0.|<s by A7,RCOMP_1:1; then
||. f/.x1 - f/.x0 .||<r by A5,A6; then
f/.x1 in N1;
hence thesis by A3;
end;
assume
A8: x0 in dom f &
for N1 being Neighbourhood of f/.x0
ex N being Neighbourhood of x0
st for x1 st x1 in dom f & x1 in N holds f/.x1 in N1;
now let r;
assume 0<r; then
reconsider N1 = { p where p is Point of S : ||. p - f/.x0 .|| < r }
as Neighbourhood of f/.x0 by NFCONT_1:3;
consider N2 being Neighbourhood of x0 such that
A9: for x1 st x1 in dom f & x1 in N2 holds f/.x1 in N1 by A8;
consider s be Real such that
A10: 0<s and
A11: N2 = ].x0-s,x0+s.[ by RCOMP_1:def 6;
take s;
for x1 st x1 in dom f & |.x1-x0.|<s holds ||. f/.x1 - f/.x0 .||<r
proof
let x1;
assume that
A12: x1 in dom f and
A13: |.x1-x0.| < s;
x1 in N2 by A11,A13,RCOMP_1:1; then
f/.x1 in N1 by A9,A12; then
ex p be Point of S st p=f/.x1 & ||. p - f/.x0 .|| < r;
hence thesis;
end;
hence 0 < s & for x1 st x1 in dom f & |.x1-x0.| < s
holds ||. f/.x1 - f/.x0 .||<r by A10;
end;
hence thesis by A8,Th8;
end;
theorem Th10:
for S,f,x0 holds
f is_continuous_in x0
iff x0 in dom f
& for N1 being Neighbourhood of f/.x0
ex N being Neighbourhood of x0 st f.:N c= N1
proof
let S,f,x0;
thus f is_continuous_in x0 implies
x0 in dom f & for N1 being Neighbourhood of f/.x0
ex N being Neighbourhood of x0 st f.:N c= N1
proof
assume A1: f is_continuous_in x0;
hence x0 in dom f;
let N1 be Neighbourhood of f/.x0;
consider N being Neighbourhood of x0 such that
A2: for x1 st x1 in dom f & x1 in N holds f/.x1 in N1 by A1,Th9;
take N;
now let r be object;
assume r in f.:N; then
consider x be Element of REAL such that
A3: x in dom f & x in N & r = f.x by PARTFUN2:59;
r=f/.x by A3,PARTFUN1:def 6;
hence r in N1 by A2,A3;
end;
hence thesis by TARSKI:def 3;
end;
assume
A4: x0 in dom f
& for N1 being Neighbourhood of f/.x0
ex N being Neighbourhood of x0 st f.:N c= N1;
now let N1 be Neighbourhood of f/.x0;
consider N being Neighbourhood of x0 such that
A5: f.:N c= N1 by A4;
take N;
let x1;
assume A6: x1 in dom f & x1 in N; then
f.x1 in f.:N by FUNCT_1:def 6; then
f/.x1 in f.:N by A6,PARTFUN1:def 6;
hence f/.x1 in N1 by A5;
end;
hence thesis by A4,Th9;
end;
theorem
(ex N be Neighbourhood of x0 st dom f /\ N = {x0})
implies f is_continuous_in x0
proof
given N be Neighbourhood of x0 such that
A1: dom f /\ N = {x0};
x0 in dom f /\ N by A1,TARSKI:def 1; then
A2:x0 in dom f by XBOOLE_0:def 4;
now let N1 be Neighbourhood of f/.x0;
take N;
A3: f/.x0 in N1 by NFCONT_1:4;
f.:N = Im(f,x0) by A1,RELAT_1:112
.= {f.x0} by A2,FUNCT_1:59
.= {f/.x0} by A2,PARTFUN1:def 6;
hence f.:N c= N1 by A3,ZFMISC_1:31;
end;
hence thesis by Th10,A2;
end;
theorem
x0 in dom f1 /\ dom f2 & f1 is_continuous_in x0 & f2 is_continuous_in x0
implies f1+f2 is_continuous_in x0 & f1-f2 is_continuous_in x0
proof
assume A1: x0 in dom f1 /\ dom f2;
assume that
A2: f1 is_continuous_in x0 & f2 is_continuous_in x0;
A3:dom (f1+f2) = dom f1 /\ dom f2 by VFUNCT_1:def 1;
A4:x0 in dom (f1+f2) by A1,VFUNCT_1:def 1;
now let s1;
assume that
A5: rng s1 c= dom(f1+f2) and
A6: s1 is convergent & lim s1=x0;
A7: rng s1 c= dom f1 /\ dom f2 by A5,VFUNCT_1:def 1;
dom (f1+f2) c= dom f1 & dom (f1+f2) c= dom f2 by A3,XBOOLE_1:17; then
A8: rng s1 c= dom f1 & rng s1 c= dom f2 by A5,XBOOLE_1:1; then
A9: f1/*s1 is convergent & f2/*s1 is convergent by A2,A6; then
f1/*s1+f2/*s1 is convergent by NORMSP_1:19;
hence (f1+f2)/*s1 is convergent by A7,Th2;
A10: f1/.x0 = lim (f1/*s1) & f2/.x0 = lim (f2/*s1) by A2,A6,A8;
thus (f1+f2)/.x0 = f1/.x0 + f2/.x0 by A4,VFUNCT_1:def 1
.= lim (f1/*s1 + f2/*s1) by A9,A10,NORMSP_1:25
.= lim ((f1+f2)/*s1) by A7,Th2;
end;
hence f1+f2 is_continuous_in x0 by A4;
A11:dom (f1-f2) = dom f1 /\ dom f2 by VFUNCT_1:def 2;
A12:x0 in dom (f1-f2) by A1,VFUNCT_1:def 2;
now let s1;
assume that
A13: rng s1 c= dom(f1-f2) and
A14: s1 is convergent & lim s1=x0;
A15:rng s1 c= dom f1 /\ dom f2 by A13,VFUNCT_1:def 2;
dom (f1-f2) c= dom f1 & dom (f1-f2) c= dom f2 by A11,XBOOLE_1:17; then
A16:rng s1 c= dom f1 & rng s1 c= dom f2 by A13,XBOOLE_1:1; then
A17:f1/*s1 is convergent & f2/*s1 is convergent by A2,A14; then
f1/*s1-f2/*s1 is convergent by NORMSP_1:20;
hence (f1-f2)/*s1 is convergent by A15,Th2;
A18:f1/.x0 = lim (f1/*s1) & f2/.x0 = lim (f2/*s1) by A2,A14,A16;
thus (f1-f2)/.x0 = f1/.x0 - f2/.x0 by A12,VFUNCT_1:def 2
.= lim (f1/*s1 - f2/*s1) by A18,A17,NORMSP_1:26
.= lim ((f1-f2)/*s1) by A15,Th2;
end;
hence f1-f2 is_continuous_in x0 by A12;
end;
theorem Th13:
f is_continuous_in x0 implies r(#)f is_continuous_in x0
proof
assume A1: f is_continuous_in x0; then
x0 in dom f;
hence A2: x0 in dom (r(#)f) by VFUNCT_1:def 4;
let s1;
assume that
A3: rng s1 c= dom(r(#)f) and
A4: s1 is convergent & lim s1=x0;
A5:rng s1 c= dom f by A3,VFUNCT_1:def 4; then
A6:f/.x0 = lim (f/*s1) by A1,A4;
A7:f/*s1 is convergent by A1,A4,A5; then
r*(f/*s1) is convergent by NORMSP_1:22;
hence (r(#)f)/*s1 is convergent by A5,Th4;
thus (r(#)f)/.x0 = r*f/.x0 by A2,VFUNCT_1:def 4
.= lim (r*(f/*s1)) by A7,A6,NORMSP_1:28
.= lim ((r(#)f)/*s1) by A5,Th4;
end;
theorem
x0 in dom f & f is_continuous_in x0
implies ||.f.|| is_continuous_in x0 & -f is_continuous_in x0
proof
assume A1: x0 in dom f;
assume A2: f is_continuous_in x0;
A3:x0 in dom ||.f.|| by A1,NORMSP_0:def 3;
now let s1;
assume that
A4: rng s1 c= dom ||.f.|| and
A5: s1 is convergent & lim s1=x0;
A6: rng s1 c= dom f by A4,NORMSP_0:def 3; then
A7: f/.x0 = lim (f/*s1) by A2,A5;
A8: f/*s1 is convergent by A2,A5,A6; then
||.f/*s1.|| is convergent by NORMSP_1:23;
hence ||.f.||/*s1 is convergent by A6,Th5;
thus (||.f.||).x0 =||. f/.x0 .|| by A3,NORMSP_0:def 3
.= lim ||.f/*s1.|| by A8,A7,LOPBAN_1:20
.= lim (||.f.||/*s1) by A6,Th5;
end;
hence ||.f.|| is_continuous_in x0;
(-1)(#)f is_continuous_in x0 by A2,Th13;
hence thesis by VFUNCT_1:23;
end;
theorem
for f1 be PartFunc of REAL,the carrier of S,
f2 be PartFunc of the carrier of S,the carrier of T
st x0 in dom (f2*f1) & f1 is_continuous_in x0
& f2 is_continuous_in f1/.x0
holds f2*f1 is_continuous_in x0
proof
let f1 be PartFunc of REAL,the carrier of S,
f2 be PartFunc of the carrier of S,the carrier of T;
assume A1: x0 in dom (f2*f1);
assume that
A2: f1 is_continuous_in x0 and
A3: f2 is_continuous_in f1/.x0;
thus x0 in dom (f2*f1) by A1;
let s1 such that
A4: rng s1 c= dom (f2*f1) and
A5: s1 is convergent & lim s1 = x0;
A6:dom (f2*f1) c= dom f1 by RELAT_1:25;
now let x be object;
assume x in rng (f1/*s1); then
consider n being Element of NAT such that
A7: x=(f1/*s1).n by FUNCT_2:113;
s1.n in rng s1 by VALUED_0:28; then
f1.(s1.n) in dom f2 by A4,FUNCT_1:11;
hence x in dom f2 by A4,A6,A7,FUNCT_2:108,XBOOLE_1:1;
end; then
A8:rng (f1/*s1) c= dom f2 by TARSKI:def 3;
A9:now let n be Element of NAT;
s1.n in rng s1 by VALUED_0:28; then
A10: s1.n in dom f1 by A4,FUNCT_1:11;
thus ((f2*f1)/*s1).n = (f2*f1).(s1.n) by A4,FUNCT_2:108
.= f2.(f1.(s1.n)) by A10,FUNCT_1:13
.= f2.((f1/*s1).n) by A4,A6,FUNCT_2:108,XBOOLE_1:1
.= (f2/*(f1/*s1)).n by A8,FUNCT_2:108;
end; then
A11:f2/*(f1/*s1) = (f2*f1)/*s1 by FUNCT_2:63;
rng s1 c= dom f1 by A4,A6,XBOOLE_1:1; then
A12: f1/*s1 is convergent & f1/.x0 = lim (f1/*s1) by A2,A5;
(f2*f1)/.x0 =f2/.(f1/.x0) by A1,PARTFUN2:3
.= lim (f2/*(f1/*s1)) by A12,A3,A8,NFCONT_1:def 5
.= lim ((f2*f1)/*s1) by A9,FUNCT_2:63;
hence thesis by A3,A12,A8,A11,NFCONT_1:def 5;
end;
definition let S,f;
attr f is continuous means :Def2:
for x0 st x0 in dom f holds f is_continuous_in x0;
end;
theorem Th16:
for X,f st X c= dom f holds f|X is continuous
iff for s1 st rng s1 c= X & s1 is convergent & lim s1 in X
holds f/*s1 is convergent & f/.(lim s1) = lim (f/*s1)
proof
let X,f such that
A1: X c= dom f;
thus f|X is continuous implies for s1 st rng s1 c= X & s1 is convergent &
lim s1 in X holds f/*s1 is convergent & f/.(lim s1) = lim (f/*s1)
proof
assume A2: f|X is continuous;
hereby let s1 such that
A3: rng s1 c= X and
A4: s1 is convergent and
A5: lim s1 in X;
A6: dom (f|X) = dom f /\ X by RELAT_1:61
.= X by A1,XBOOLE_1:28; then
A7: f|X is_continuous_in (lim s1) by A2,A5;
now let n be Element of NAT;
A8: s1.n in rng s1 by VALUED_0:28;
thus ((f|X)/*s1).n = (f|X)/.(s1.n) by A3,A6,FUNCT_2:109
.= f/.(s1.n) by A3,A6,A8,PARTFUN2:15
.= (f/*s1).n by A1,A3,FUNCT_2:109,XBOOLE_1:1;
end; then
A9: (f|X)/*s1 = f/*s1 by FUNCT_2:63;
lim s1 in REAL by XREAL_0:def 1;
then f/.(lim s1) = (f|X)/.(lim s1) by A5,A6,PARTFUN2:15
.= lim (f/*s1) by A3,A4,A6,A7,A9;
hence f/*s1 is convergent & f/.(lim s1) = lim (f/*s1)
by A3,A4,A6,A7,A9;
end;
end;
assume
A10:for s1 st rng s1 c= X & s1 is convergent & lim s1 in X
holds f/*s1 is convergent & f/.(lim s1) = lim (f/*s1);
now
A11: dom (f|X) = dom f /\ X by RELAT_1:61
.= X by A1,XBOOLE_1:28;
let x1 such that
A12: x1 in dom(f|X);
now let s1 such that
A13: rng s1 c= dom (f|X) and
A14: s1 is convergent and
A15: lim s1 = x1;
now let n be Element of NAT;
A16: s1.n in rng s1 by VALUED_0:28;
thus ((f|X)/*s1).n = (f|X)/.(s1.n) by A13,FUNCT_2:109
.= f/.(s1.n) by A13,A16,PARTFUN2:15
.= (f/*s1).n by A1,A11,A13,FUNCT_2:109,XBOOLE_1:1;
end; then
A17: (f|X)/*s1 = f/*s1 by FUNCT_2:63;
lim s1 in REAL by XREAL_0:def 1;
then (f|X)/.(lim s1) = f/.(lim s1) by A12,A15,PARTFUN2:15
.= lim ((f|X)/*s1) by A10,A12,A11,A13,A14,A15,A17;
hence (f|X)/*s1 is convergent & (f|X)/.x1 = lim ((f|X)/*s1)
by A10,A12,A11,A13,A14,A15,A17;
end;
hence f|X is_continuous_in x1 by A12;
end;
hence thesis;
end;
theorem Th17:
X c= dom f implies
(f|X is continuous
iff for x0,r st x0 in X & 0 < r ex s
st 0 < s & for x1 st x1 in X & |.x1-x0.| < s
holds ||. f/.x1 - f/.x0 .|| < r)
proof
assume A1: X c= dom f;
thus f|X is continuous implies for x0,r st x0 in X & 0<r ex s st 0<s & for
x1 st x1 in X & |.x1-x0.| < s holds ||. f/.x1 - f/.x0 .|| < r
proof
assume A2: f|X is continuous;
let x0,r;
assume that
A3: x0 in X and
A4: 0 < r;
x0 in dom(f|X) by A1,A3,RELAT_1:62; then
f|X is_continuous_in x0 by A2; then
consider s such that
A5: 0 < s and
A6: for x1 st x1 in dom(f|X) & |.x1-x0.| < s
holds ||.(f|X)/.x1-(f|X)/.x0 .|| < r by A4,Th8;
take s;
thus 0<s by A5;
let x1;
assume that
A7: x1 in X and
A8: |.x1-x0.|<s;
A9: x0 in REAL by XREAL_0:def 1;
A10: x1 in REAL by XREAL_0:def 1;
A11: dom (f|X) = dom f /\ X by RELAT_1:61
.= X by A1,XBOOLE_1:28; then
||. f/.x1 - f/.x0 .||
= ||.(f|X)/.x1 - f/.x0 .|| by A7,A10,PARTFUN2:15
.= ||.(f|X)/.x1 - (f|X)/.x0 .|| by A3,A11,A9,PARTFUN2:15;
hence thesis by A6,A11,A7,A8;
end;
assume
A12:for x0,r st x0 in X & 0 <r
ex s st 0 < s & for x1 st x1 in X & |.x1-x0.| < s
holds ||. f/.x1 - f/.x0 .|| < r;
now let x0;
assume A13: x0 in dom(f|X); then
A14:x0 in X;
for r st 0 < r ex s st 0 < s & for x1 st x1 in dom(f|X) & |.x1-x0.| < s
holds ||.(f|X)/.x1-(f|X)/.x0 .||<r
proof
let r;
assume 0 < r; then
consider s such that
A15: 0<s and
A16: for x1 st x1 in X & |.x1-x0.| < s holds ||. f/.x1 - f/.x0 .|| < r
by A12,A14;
take s;
thus 0<s by A15;
let x1 such that
A17: x1 in dom(f|X) and
A18: |.x1-x0.|<s;
A19: x0 in REAL by XREAL_0:def 1;
A20: x1 in REAL by XREAL_0:def 1;
||.(f|X)/.x1-(f|X)/.x0 .||
= ||.(f|X)/.x1 - f/.x0 .|| by A13,A19,PARTFUN2:15
.= ||. f/.x1 - f/.x0 .|| by A17,A20,PARTFUN2:15;
hence thesis by A16,A17,A18;
end;
hence f|X is_continuous_in x0 by Th8,A13;
end;
hence thesis;
end;
registration let S;
cluster constant -> continuous for PartFunc of REAL,the carrier of S;
coherence
proof
let f be PartFunc of REAL,the carrier of S;
assume A1: f is constant;
now
reconsider s = 1 as Real;
let x0,r;
assume that
A2: x0 in dom f and
A3: 0<r;
take s;
thus 0<s;
let x1;
assume A4: x1 in dom f;
assume |.x1-x0.| < s;
f/.x1 = f.x1 by A4,PARTFUN1:def 6
.= f.x0 by A1,A2,A4,FUNCT_1:def 10
.= f/.x0 by A2,PARTFUN1:def 6;
hence ||. f/.x1 - f/.x0 .|| < r by A3,NORMSP_1:6;
end; then
f|dom f is continuous by Th17;
hence thesis;
end;
end;
registration let S;
cluster continuous for PartFunc of REAL,the carrier of S;
existence
proof
set f = the constant PartFunc of REAL,the carrier of S;
take f;
thus thesis;
end;
end;
registration let S;
let f be continuous PartFunc of REAL,the carrier of S, X be set;
cluster f|X -> continuous for PartFunc of REAL,the carrier of S;
coherence
proof
now let x0;
assume A1: x0 in dom(f|X); then
x0 in dom f by RELAT_1:57; then
A2: f is_continuous_in x0 by Def2;
x0 in X by A1;
hence f|X is_continuous_in x0 by A2,Th6;
end;
hence thesis;
end;
end;
theorem Th18:
f|X is continuous & X1 c= X implies f|X1 is continuous
proof
assume A1: f|X is continuous;
assume X1 c= X; then
f|X1 = f|X|X1 by RELAT_1:74;
hence thesis by A1;
end;
registration let S;
cluster empty -> continuous for PartFunc of REAL,the carrier of S;
coherence;
end;
registration let S,f;
let X be trivial set;
cluster f|X -> continuous for PartFunc of REAL,the carrier of S;
coherence
proof
now assume f|X is not empty; then
consider x0 such that
A1: x0 in dom(f|X qua PartFunc of REAL,the carrier of S) by MEMBERED:9;
x0 in X by A1,RELAT_1:57; then
A2: X = {x0} by ZFMISC_1:132;
now let p be Real;
assume A3: p in dom(f|X); then
A4: p in {x0} by A2;
thus f|X is_continuous_in p
proof
thus p in dom (f|X) by A3;
let s1;
assume that
A5: rng s1 c= dom(f|X) and
s1 is convergent and
lim s1=p;
A6: dom f /\ {x0} c= {x0} by XBOOLE_1:17;
rng s1 c= dom f /\ {x0} by A2,A5,RELAT_1:61; then
A7: rng s1 c= {x0} by A6,XBOOLE_1:1;
A8: now let n;
s1.n in rng s1 by VALUED_0:28;
hence s1.n = x0 by A7,TARSKI:def 1;
end;
A9: p=x0 by A4,TARSKI:def 1;
A10: now let g be Real such that
A11: 0<g;
reconsider n=0 as Nat;
take n;
let m such that n<=m;
A12: m in NAT by ORDINAL1:def 12;
||.((f|{x0})/*s1).m - (f|{x0})/.p .||
= ||.(f|{x0})/.(s1.m) - (f|{x0})/.x0 .|| by A2,A9,A5,FUNCT_2:109,A12
.= ||.(f|{x0})/.x0 - (f|{x0})/.x0 .|| by A8
.= 0 by NORMSP_1:6;
hence ||.((f|{x0})/*s1).m - (f|{x0})/.p .|| < g by A11;
end;
hence (f|X)/*s1 is convergent by A2,NORMSP_1:def 6;
hence lim ((f|X)/*s1) = ((f|X))/.p by A2,A10,NORMSP_1:def 7;
end;
end;
hence thesis;
end;
hence thesis;
end;
end;
registration
let S;
let f1,f2 be continuous PartFunc of REAL,the carrier of S;
cluster f1+f2 -> continuous for PartFunc of REAL,the carrier of S;
coherence
proof
set X = dom(f1+f2);
X c= dom f1 /\ dom f2 by VFUNCT_1:def 1; then
A1:X c= dom f1 & X c= dom f2 by XBOOLE_1:18;
A2:f1|X is continuous & f2|X is continuous;
now let s1;
assume that
A3: rng s1 c= X and
A4: s1 is convergent and
A5: lim s1 in X;
A6: f1/*s1 is convergent & f2/*s1 is convergent by A1,A2,A3,A4,A5,Th16; then
A7: (f1/*s1)+(f2/*s1) is convergent by NORMSP_1:19;
A8: rng s1 c= dom f1 /\ dom f2 by A3,VFUNCT_1:def 1;
f1/.(lim s1) = lim (f1/*s1) & f2/.(lim s1) = lim (f2/*s1)
by A1,A2,A3,A4,A5,Th16; then
(f1+f2)/.(lim s1) = lim (f1/*s1) + lim (f2/*s1) by A5,VFUNCT_1:def 1
.= lim (f1/*s1 + f2/*s1) by A6,NORMSP_1:25
.= lim ((f1+f2)/*s1) by A8,Th2;
hence (f1+f2)/*s1 is convergent & (f1+f2)/.(lim s1)=lim((f1+f2)/*s1)
by A8,A7,Th2;
end; then
(f1+f2)|X is continuous by Th16;
hence thesis;
end;
cluster f1-f2 -> continuous for PartFunc of REAL,the carrier of S;
coherence
proof
set X = dom(f1-f2);
X c= dom f1 /\ dom f2 by VFUNCT_1:def 2; then
A9:X c= dom f1 & X c= dom f2 by XBOOLE_1:18;
A10: f1|X is continuous & f2|X is continuous;
now let s1;
assume that
A11: rng s1 c= X and
A12: s1 is convergent and
A13: lim s1 in X;
A14:f1/*s1 is convergent & f2/*s1 is convergent
by A9,A10,A11,A12,A13,Th16; then
A15:(f1/*s1)-(f2/*s1) is convergent by NORMSP_1:20;
A16:rng s1 c= dom f1 /\ dom f2 by A11,VFUNCT_1:def 2;
f1/.(lim s1) = lim (f1/*s1) & f2/.(lim s1) = lim (f2/*s1)
by A9,A10,A11,A12,A13,Th16; then
(f1-f2)/.(lim s1) = lim (f1/*s1) - lim (f2/*s1) by A13,VFUNCT_1:def 2
.= lim (f1/*s1 - f2/*s1) by A14,NORMSP_1:26
.= lim ((f1-f2)/*s1) by A16,Th2;
hence (f1-f2)/*s1 is convergent & (f1-f2)/.(lim s1)=lim((f1-f2)/*s1)
by A16,A15,Th2;
end; then
(f1-f2) |X is continuous by Th16;
hence thesis;
end;
end;
theorem Th19:
for X,f1,f2 st X c= dom f1 /\ dom f2 & f1|X is continuous & f2|X is continuous
holds (f1+f2)|X is continuous & (f1-f2)|X is continuous
proof
let X,f1,f2;
assume that
A1: X c= dom f1 /\ dom f2 and
A2: f1|X is continuous & f2|X is continuous;
A3:X c= dom f1 & X c= dom f2 by A1,XBOOLE_1:18;
A4:X c= dom (f1+f2) & X c= dom (f1-f2) by A1,VFUNCT_1:def 1,def 2;
now let s1;
assume that
A5: rng s1 c= X & s1 is convergent and
A6: lim s1 in X;
A7:f1/*s1 is convergent & f2/*s1 is convergent by A3,A2,A5,A6,Th16; then
A8:(f1/*s1)+(f2/*s1) is convergent by NORMSP_1:19;
A9:rng s1 c= dom f1 /\ dom f2 by A1,A5,XBOOLE_1:1;
A10: lim s1 in REAL by XREAL_0:def 1;
f1/.(lim s1) = lim (f1/*s1) & f2/.(lim s1) = lim (f2/*s1)
by A3,A2,A5,A6,Th16; then
(f1+f2)/.(lim s1) = lim (f1/*s1) + lim (f2/*s1) by A4,A6,VFUNCT_1:def 1,A10
.= lim (f1/*s1 + f2/*s1) by A7,NORMSP_1:25
.= lim ((f1+f2)/*s1) by A9,Th2;
hence (f1+f2)/*s1 is convergent & (f1+f2)/.(lim s1)=lim((f1+f2)/*s1)
by A9,A8,Th2;
end;
hence (f1+f2)|X is continuous by A4,Th16;
now let s1;
assume that
A11: rng s1 c= X & s1 is convergent and
A12: lim s1 in X;
A13:f1/*s1 is convergent & f2/*s1 is convergent by A3,A2,A11,A12,Th16; then
A14:(f1/*s1)-(f2/*s1) is convergent by NORMSP_1:20;
A15:rng s1 c= dom f1 /\ dom f2 by A1,A11,XBOOLE_1:1;
A16: lim s1 in REAL by XREAL_0:def 1;
f1/.(lim s1) = lim (f1/*s1) & f2/.(lim s1) = lim (f2/*s1)
by A3,A2,A11,A12,Th16; then
(f1-f2)/.(lim s1) = lim (f1/*s1) - lim (f2/*s1) by A4,A12,VFUNCT_1:def 2,
A16
.= lim (f1/*s1 - f2/*s1) by A13,NORMSP_1:26
.= lim ((f1-f2)/*s1) by A15,Th2;
hence (f1-f2)/*s1 is convergent & (f1-f2)/.(lim s1)=lim((f1-f2)/*s1)
by A15,A14,Th2;
end;
hence (f1-f2)|X is continuous by A4,Th16;
end;
theorem
for X,X1,f1,f2 st X c= dom f1 & X1 c= dom f2
& f1|X is continuous & f2|X1 is continuous
holds (f1+f2)|(X /\ X1) is continuous & (f1-f2)|(X /\ X1) is continuous
proof
let X,X1,f1,f2;
assume X c= dom f1 & X1 c= dom f2; then
A1:X /\ X1 c= dom f1 /\ dom f2 by XBOOLE_1:27;
assume f1|X is continuous & f2|X1 is continuous; then
f1|(X /\ X1) is continuous & f2|(X /\ X1) is continuous by Th18,XBOOLE_1:17;
hence thesis by A1,Th19;
end;
registration
let S;
let f be continuous PartFunc of REAL,the carrier of S;
let r;
cluster r(#)f -> continuous for PartFunc of REAL,the carrier of S;
coherence
proof
set X = dom f;
A1:X = dom(r(#)f) by VFUNCT_1:def 4; then
A2:(r(#)f) |X = r(#)f;
now let s1;
assume that
A3: rng s1 c= X and
A4: s1 is convergent and
A5: lim s1 in X;
f|X is continuous; then
A6: f/*s1 is convergent & f/.(lim s1) = lim (f/*s1) by A3,A4,A5,Th16; then
A7: r*(f/*s1) is convergent by NORMSP_1:22;
(r(#)f)/.(lim s1) = r * lim (f/*s1) by A1,A5,A6,VFUNCT_1:def 4
.= lim (r*(f/*s1)) by A6,NORMSP_1:28
.= lim ((r(#)f)/*s1) by A3,Th4;
hence (r(#)f)/*s1 is convergent & (r(#)f)/.(lim s1)=lim((r(#)f)/*s1)
by A3,A7,Th4;
end;
hence thesis by A1,A2,Th16;
end;
end;
theorem Th21:
X c= dom f & f|X is continuous implies (r(#)f)|X is continuous
proof
assume that
A1: X c= dom f and
A2: f|X is continuous;
A3:X c= dom(r(#)f) by A1,VFUNCT_1:def 4;
now let s1;
assume that
A4: rng s1 c= X & s1 is convergent and
A5: lim s1 in X;
A6: f/*s1 is convergent by A1,A2,A4,A5,Th16; then
A7: r*(f/*s1) is convergent by NORMSP_1:22;
A8: lim s1 in REAL by XREAL_0:def 1;
f/.(lim s1) = lim (f/*s1) by A1,A2,A4,A5,Th16;
then (r(#)f)/.(lim s1) = r * lim (f/*s1) by A3,A5,VFUNCT_1:def 4,A8
.= lim (r*(f/*s1)) by A6,NORMSP_1:28
.= lim ((r(#)f)/*s1) by A1,A4,Th4,XBOOLE_1:1;
hence (r(#)f)/*s1 is convergent & (r(#)f)/.(lim s1)=lim((r(#)f)/*s1)
by A1,A4,A7,Th4,XBOOLE_1:1;
end;
hence thesis by A3,Th16;
end;
theorem
X c= dom f & f|X is continuous
implies (||.f.||)|X is continuous & (-f)|X is continuous
proof
assume that
A1: X c= dom f and
A2: f|X is continuous;
thus (||.f.||)|X is continuous
proof
let r be Real;
assume A3: r in dom((||.f.||)|X); then
A4:r in dom ||.f.|| & r in X by RELAT_1:57; then
r in dom f by NORMSP_0:def 3; then
A5: r in dom(f|X) by A4,RELAT_1:57; then
A6: f|X is_continuous_in r by A2;
thus (||.f.||)|X is_continuous_in r
proof
let s1;
assume that
A7: rng s1 c= dom ((||.f.||)|X) and
A8: s1 is convergent & lim s1 = r;
rng s1 c= dom (||.f.||) /\ X by A7,RELAT_1:61; then
rng s1 c= dom f /\ X by NORMSP_0:def 3; then
A9: rng s1 c= dom (f|X) by RELAT_1:61;
now let n be Element of NAT;
A10: s1.n in rng s1 by VALUED_0:28; then
s1.n in dom (f|X) by A9; then
s1.n in dom f /\ X by RELAT_1:61; then
A11: s1.n in X & s1.n in dom f by XBOOLE_0:def 4; then
A12: s1.n in dom (||.f.||) by NORMSP_0:def 3;
thus ||. (f|X)/*s1 .|| .n = ||. ((f|X)/*s1).n .|| by NORMSP_0:def 4
.=||.(f|X)/.(s1.n) .|| by A9,FUNCT_2:109
.=||. f/.(s1.n) .|| by A9,A10,PARTFUN2:15
.=(||.f.||).(s1.n) by A12,NORMSP_0:def 3
.=((||.f.||)|X).(s1.n) by A11,FUNCT_1:49
.=(((||.f.||)|X)/*s1).n by A7,FUNCT_2:108;
end; then
A13: ||.(f|X)/*s1 .|| = ((||.f.||)|X)/*s1 by FUNCT_2:63;
r in REAL by XREAL_0:def 1;
then
A14: ||.(f|X)/.r.|| = ||. f/.r .|| by A5,PARTFUN2:15
.= (||.f.||).r by A4,NORMSP_0:def 3
.= ((||.f.||)|X).r by A3,FUNCT_1:47;
A15: (f|X)/*s1 is convergent by A6,A8,A9;
hence ((||.f.||)|X)/*s1 is convergent by A13,NORMSP_1:23;
(f|X)/.r = lim ((f|X)/*s1) by A6,A8,A9;
hence thesis by A15,A13,A14,LOPBAN_1:20;
end;
end;
((-1)(#)f)|X is continuous by A1,A2,Th21;
hence thesis by VFUNCT_1:23;
end;
theorem
f is total & (for x1,x2 holds f/.(x1+x2) = f/.x1 + f/.x2)
& (ex x0 st f is_continuous_in x0)
implies f|REAL is continuous
proof
assume that
A1: f is total and
A2: for x1,x2 holds f/.(x1+x2) = f/.x1 + f/.x2;
A3:dom f = REAL by A1,PARTFUN1:def 2;
given x0 such that
A4: f is_continuous_in x0;
reconsider z0=0 as Real;
f/.z0 + f/.z0 = f/.(z0+z0) by A2; then
f/.z0 + (f/.z0 - f/.z0) = f/.z0 - f/.z0 by RLVECT_1:28; then
f/.z0 + 0.S = f/.z0 - f/.z0 by RLVECT_1:15; then
A5:f/.z0 + 0.S = 0.S by RLVECT_1:15;
A6:now let x1;
0.S = f/.(x1+-x1) by A5,RLVECT_1:4; then
0.S = f/.x1+f/.(-x1) by A2;
hence -(f/.x1)=f/.(-x1) by RLVECT_1:def 10;
end;
A7:now let x1,x2;
f/.(x1-x2) = f/.(x1+-x2); then
f/.(x1-x2) = f/.x1 + f/.(-x2) by A2;
hence f/.(x1-x2) = f/.x1 - f/.x2 by A6;
end;
now let x1,r;
assume that
x1 in REAL and
A8: r>0;
set y=x1-x0;
consider s such that
A9: 0<s and
A10: for x1 st x1 in dom f & |.x1-x0.|<s holds ||. f/.x1 - f/.x0 .||<r
by A4,A8,Th8;
take s;
thus s>0 by A9;
let x2 such that
x2 in REAL and
A11: |.x2-x1.|<s;
A12: x2-y in REAL & |.x2-y-x0.| = |.x2-x1.| by XREAL_0:def 1;
y+x0=x1; then
||.f/.x2-f/.x1.|| = ||.f/.x2-(f/.y+f/.x0).|| by A2
.= ||.f/.x2-f/.y-f/.x0 .|| by RLVECT_1:27
.= ||.f/.(x2-y)-f/.x0 .|| by A7;
hence ||.f/.x2-f/.x1.||<r by A3,A10,A11,A12;
end;
hence thesis by A3,Th17;
end;
theorem Th24:
dom f is compact & f|(dom f) is continuous implies rng f is compact
proof
assume that
A1: dom f is compact and
A2: f|(dom f) is continuous;
now
let s1 be sequence of S such that
A3: rng s1 c= rng f;
defpred P[set,set] means $2 in dom f & f/.$2=s1.$1;
A4:for n being Element of NAT ex p being Element of REAL st P[n,p]
proof
let n be Element of NAT;
dom s1 = NAT by FUNCT_2:def 1; then
s1.n in rng s1 by FUNCT_1:3; then
consider p be Element of REAL such that
A5: p in dom f & s1.n =f.p by A3,PARTFUN1:3;
take p;
thus thesis by A5,PARTFUN1:def 6;
end;
consider q1 be Real_Sequence such that
A6: for n being Element of NAT holds P[n,q1.n] from FUNCT_2:sch 3(A4);
now let x be object;
assume x in rng q1; then
ex n being Element of NAT st x = q1.n by FUNCT_2:113;
hence x in dom f by A6;
end; then
A7:rng q1 c= dom f by TARSKI:def 3; then
consider s2 such that
A8: s2 is subsequence of q1 and
A9: s2 is convergent and
A10:lim s2 in dom f by A1,RCOMP_1:def 3;
take q2 = f/*s2;
rng s2 c= rng q1 by A8,VALUED_0:21; then
A11: rng s2 c= dom f by A7,XBOOLE_1:1;
now
let n be Element of NAT;
f/.(q1.n)=s1.n by A6;
hence (f/*q1).n= s1.n by A7,FUNCT_2:109;
end; then
A12: f/*q1=s1 by FUNCT_2:63;
lim s2 in dom(f|(dom f)) by A10; then
f|(dom f) is_continuous_in (lim s2) by A2; then
A13: f is_continuous_in (lim s2); then
f/.(lim s2) = lim (f/*s2) by A9,A11;
hence
q2 is subsequence of s1 & q2 is convergent & (lim q2) in rng f
by A7,A12,A8,A9,A13,A11,PARTFUN2:2,VALUED_0:22;
end;
hence thesis by NFCONT_1:def 2;
end;
theorem
Y c= dom f & Y is compact & f|Y is continuous implies (f.:Y) is compact
proof
assume that
A1: Y c= dom f and
A2: Y is compact and
A3: f|Y is continuous;
A4:f|Y|Y is continuous by A3;
dom (f|Y) = dom f /\ Y by RELAT_1:61
.= Y by A1,XBOOLE_1:28; then
rng (f|Y) is compact by A2,A4,Th24;
hence thesis by RELAT_1:115;
end;
begin :: Lipschitz continuity
definition let S,f;
attr f is Lipschitzian means :Def3:
ex r be Real st 0<r & for x1,x2 st x1 in dom f &
x2 in dom f holds ||.f/.x1-f/.x2.||<=r*|.x1-x2.|;
end;
theorem Th26:
f|X is Lipschitzian
iff ex r be Real st 0<r & for x1,x2 st x1 in dom(f|X) & x2 in dom(f|X)
holds ||. f/.x1-f/.x2 .|| <= r*|.x1-x2.|
proof
thus f|X is Lipschitzian implies ex r be Real
st 0<r & for x1,x2 st x1 in dom(f|X) &
x2 in dom(f|X) holds ||.f/.x1-f/.x2.|| <= r*|.x1-x2.|
proof
given r be Real such that
A1: 0<r and
A2: for x1,x2 st x1 in dom(f|X) & x2 in dom(f|X)
holds ||.(f|X)/.x1-(f|X)/.x2.||<=r*|.x1-x2.|;
take r;
thus 0<r by A1;
let x1,x2;
A3: x1 in REAL & x2 in REAL by XREAL_0:def 1;
assume A4: x1 in dom(f|X) & x2 in dom(f|X); then
(f|X)/.x1 = f/.x1 & (f|X)/.x2 = f/.x2 by A3,PARTFUN2:15;
hence thesis by A2,A4;
end;
given r be Real such that
A5: 0<r and
A6: for x1,x2 st x1 in dom(f|X) & x2 in dom(f|X)
holds ||.f/.x1-f/.x2.|| <= r*|.x1-x2.|;
take r;
thus 0<r by A5;
let x1,x2;
A7: x1 in REAL & x2 in REAL by XREAL_0:def 1;
assume A8: x1 in dom(f|X) & x2 in dom(f|X); then
(f|X)/.x1 = f/.x1 & (f|X)/.x2 = f/.x2 by A7,PARTFUN2:15;
hence thesis by A6,A8;
end;
registration let S;
cluster empty -> 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<r and
A2: for x1,x2 st x1 in dom f & x2 in dom f
holds ||.f/.x1-f/.x2.|| <= r*|.x1-x2.| by Def3;
now let x1,x2;
assume x1 in dom(f|X) & x2 in dom(f|X); then
x1 in dom f & x2 in dom f by RELAT_1:57;
hence ||.f/.x1-f/.x2.||<=r*|.x1-x2.| by A2;
end;
hence thesis by A1,Th26;
end;
end;
theorem
f|X is Lipschitzian & X1 c= X implies f|X1 is Lipschitzian
proof
assume that
A1: f|X is Lipschitzian and
A2: X1 c= X;
f|X1 = f|X|X1 by A2,RELAT_1:74;
hence thesis by A1;
end;
registration
let S;
let f1,f2 be Lipschitzian PartFunc of REAL,the carrier of S;
cluster f1+f2 -> Lipschitzian for PartFunc of REAL,the carrier of S;
coherence
proof
set X = dom f1, X1 = dom f2;
consider s such that
A1: 0<s and
A2: for x1,x2 st x1 in dom(f1|(X /\ X1)) & x2 in dom(f1|(X /\ X1))
holds ||.f1/.x1-f1/.x2.||<=s*|.x1-x2.| by Th26;
consider g such that
A3: 0<g and
A4: for x1,x2 st x1 in dom(f2|(X /\ X1)) & x2 in dom(f2|(X /\ X1))
holds ||.f2/.x1-f2/.x2.||<=g*|.x1-x2.| by Th26;
now
take p=s+g;
thus 0<p by A1,A3;
let x1,x2;
assume A5: x1 in dom(f1+f2) & x2 in dom(f1+f2);
||.(f1+f2)/.x1-(f1+f2)/.x2.||
= ||.f1/.x1 + f2/.x1-(f1+f2)/.x2.|| by A5,VFUNCT_1:def 1
.= ||.f1/.x1 + f2/.x1 - (f1/.x2+f2/.x2).|| by A5,VFUNCT_1:def 1
.= ||. f1/.x1 + (f2/.x1 - (f1/.x2+f2/.x2)).|| by RLVECT_1:28
.= ||. f1/.x1 + (f2/.x1 - f1/.x2-f2/.x2).|| by RLVECT_1:27
.= ||. f1/.x1 + (-f1/.x2 + f2/.x1-f2/.x2).||
.= ||. f1/.x1 + (-f1/.x2 + (f2/.x1-f2/.x2)).|| by RLVECT_1:28
.= ||. f1/.x1 - f1/.x2 + (f2/.x1-f2/.x2).|| by RLVECT_1:def 3; then
A6: ||. (f1+f2)/.x1-(f1+f2)/.x2.||
<= ||. f1/.x1-f1/.x2.||+||. f2/.x1-f2 /.x2.|| by NORMSP_1:def 1;
dom(f2| (X /\ X1)) = dom f2 /\ (X /\ X1) by RELAT_1:61
.= dom f2 /\ X1 /\ X by XBOOLE_1:16
.= dom(f1+f2) by VFUNCT_1:def 1; then
A7: ||.f2/.x1-f2/.x2 .||<=g*|.x1-x2.| by A4,A5;
dom(f1|(X /\ X1)) = dom f1 /\ (X /\ X1) by RELAT_1:61
.= dom f1 /\ X /\ X1 by XBOOLE_1:16
.= dom(f1+f2) by VFUNCT_1:def 1; then
||.f1/.x1-f1/.x2.||<=s*|.x1-x2.| by A2,A5; then
||.f1/.x1-f1/.x2.||+||.f2/.x1-f2/.x2.||
<= s*|.x1-x2.| + g*|.x1-x2.| by A7,XREAL_1:7;
hence ||.(f1+f2)/.x1-(f1+f2)/.x2.||<=p*|.x1-x2.| by A6,XXREAL_0:2;
end;
hence thesis;
end;
cluster f1-f2 -> Lipschitzian for PartFunc of REAL,the carrier of S;
coherence
proof
set X = dom f1, X1 = dom f2;
consider s such that
A8: 0<s and
A9:for x1,x2 st x1 in dom(f1|(X /\ X1)) & x2 in dom(f1|(X /\ X1))
holds ||.f1/.x1-f1/.x2.||<=s*|.x1-x2.| by Th26;
consider g be Real such that
A10:0<g and
A11:for x1,x2 st x1 in dom(f2|(X /\ X1)) & x2 in dom(f2|(X /\ X1))
holds ||.f2/.x1-f2/.x2.||<=g*|.x1-x2.| by Th26;
now
take p=s+g;
thus 0<p by A8,A10;
let x1,x2;
assume A12: x1 in dom(f1-f2) & x2 in dom(f1-f2);
||.(f1-f2)/.x1-(f1-f2)/.x2.||
= ||.f1/.x1 - f2/.x1-(f1-f2)/.x2.|| by A12,VFUNCT_1:def 2
.= ||.f1/.x1 - f2/.x1 - (f1/.x2-f2/.x2).|| by A12,VFUNCT_1:def 2
.= ||. f1/.x1 - (f2/.x1 + (f1/.x2-f2/.x2)).|| by RLVECT_1:27
.= ||. f1/.x1 - (f1/.x2 + f2/.x1-f2/.x2).|| by RLVECT_1:28
.= ||. f1/.x1 - (f1/.x2 + (f2/.x1-f2/.x2)).|| by RLVECT_1:28
.= ||. f1/.x1 - f1/.x2 - (f2/.x1-f2/.x2).|| by RLVECT_1:27; then
A13:||. (f1-f2)/.x1-(f1-f2)/.x2.||
<= ||. f1/.x1-f1/.x2.||+||. f2/.x1-f2 /.x2.|| by NORMSP_1:3;
dom(f2|(X /\ X1)) = dom f2 /\ (X /\ X1) by RELAT_1:61
.= dom f2 /\ X1 /\ X by XBOOLE_1:16
.= dom(f1-f2) by VFUNCT_1:def 2; then
A14:||.f2/.x1-f2/.x2.||<=g*|.x1-x2.| by A11,A12;
dom(f1|(X /\ X1)) = dom f1 /\ (X /\ X1) by RELAT_1:61
.= dom f1 /\ X /\ X1 by XBOOLE_1:16
.= dom(f1-f2) by VFUNCT_1:def 2; then
||.f1/.x1-f1/.x2.||<=s*|.x1-x2.| by A9,A12; then
||.f1/.x1-f1/.x2.||+||.f2/.x1-f2/.x2.||
<= s*|.x1-x2.|+g*|.x1-x2.| by A14,XREAL_1:7;
hence ||.(f1-f2)/.x1-(f1-f2)/.x2.||<=p*|.x1-x2.| by A13,XXREAL_0:2;
end;
hence thesis;
end;
end;
theorem
f1|X is Lipschitzian & f2|X1 is Lipschitzian
implies (f1+f2)|(X /\ X1) is Lipschitzian
proof
A1:f1|(X /\ X1) = f1|X|(X /\ X1) & f2|(X /\ X1) = f2|X1|(X /\ X1)
by RELAT_1:74,XBOOLE_1:17;
A2:(f1+f2)|(X /\ X1) = f1|(X /\ X1) + f2|(X /\ X1) by VFUNCT_1:27;
assume f1|X is Lipschitzian & f2|X1 is Lipschitzian;
hence thesis by A1,A2;
end;
theorem
f1|X is Lipschitzian & f2|X1 is Lipschitzian
implies (f1-f2)|(X /\ X1) is Lipschitzian
proof
A1:f1|(X /\ X1) = f1|X|(X /\ X1) & f2|(X /\ X1) = f2|X1|(X /\ X1)
by RELAT_1:74,XBOOLE_1:17;
A2:(f1-f2)|(X /\ X1) = f1|(X /\ X1)-f2|(X /\ X1) by VFUNCT_1:30;
assume f1|X is Lipschitzian & f2|X1 is Lipschitzian;
hence thesis by A1,A2;
end;
registration
let S;
let f be Lipschitzian PartFunc of REAL, the carrier of S;
let p;
cluster p(#)f -> 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<s by A1;
let x1,x2;
assume A4: x1 in dom(p(#)f) & x2 in dom(p(#)f);
A5: 0<=|.x1-x2.| by COMPLEX1:46;
||.(p(#)f)/.x1-(p(#)f)/.x2.||
= ||.p*(f/.x1)-(p(#)f)/.x2.|| by A4,VFUNCT_1:def 4
.= ||.p*(f/.x1) - p*(f/.x2).|| by A4,VFUNCT_1:def 4
.= ||.0.S - p*(f/.x2).|| by A3,RLVECT_1:10
.= ||. 0.S - 0.S .|| by A3,RLVECT_1:10
.= 0 by NORMSP_1:6;
hence ||.(p(#)f)/.x1-(p(#)f)/.x2.||<=s*|.x1-x2.| by A1,A5;
end;
hence thesis;
end;
suppose p<>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<g by A6;
let x1,x2;
assume A8: x1 in dom(p(#)f) & x2 in dom(p(#)f); then
A9: ||.(p(#)f)/.x1-(p(#)f)/.x2.||
= ||.p*(f/.x1)-(p(#)f)/.x2.|| by VFUNCT_1:def 4
.= ||.p*(f/.x1) - p*(f/.x2).|| by A8,VFUNCT_1:def 4
.= ||.p*(f/.x1 - f/.x2).|| by RLVECT_1:34
.= |.p.|*||.f/.x1 - f/.x2.|| by NORMSP_1:def 1;
x1 in dom f & x2 in dom f by A8,VFUNCT_1:def 4; then
|.p.|*||.f/.x1 - f/.x2.||<=|.p.|*(s*|.x1-x2.|) by A2,A7,XREAL_1:64;
hence ||.(p(#)f)/.x1-(p(#)f)/.x2.||<=g*|.x1-x2.| by A9;
end;
hence thesis;
end;
end;
end;
theorem
f|X is Lipschitzian & X c= dom f implies (p(#)f) | X is Lipschitzian
proof
(p(#)f)|X = p(#)(f|X) by VFUNCT_1:31;
hence thesis;
end;
registration let S;
let f be Lipschitzian PartFunc of REAL, the carrier of S;
cluster ||. f .|| -> Lipschitzian for PartFunc of REAL,REAL;
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;
now let x1,x2;
assume A3:x1 in dom ||.f.|| & x2 in dom ||.f.||; then
x1 in dom f & x2 in dom f by NORMSP_0:def 3; then
A4: ||.f/.x1-f/.x2.|| <= s*|.x1-x2.| by A2;
|.(||.f.||).x1 - (||.f.||).x2.|
= |.||. f/.x1.|| - (||.f.||).x2.| by A3,NORMSP_0:def 3
.= |.||. f/.x1.|| - ||. f/.x2 .||.| by A3,NORMSP_0:def 3; then
|.(||.f.||).x1-(||.f.||).x2.| <= ||. f/.x1-f/.x2.|| by NORMSP_1:9;
hence
|.(||.f.||).x1-(||.f.||).x2.| <= s*|.x1-x2.| by A4,XXREAL_0:2;
end;
hence thesis by A1;
end;
end;
theorem
f|X is Lipschitzian
implies -(f|X) is Lipschitzian & (-f)|X is Lipschitzian
& (||.f.||)|X is Lipschitzian
proof
assume A1: f|X is Lipschitzian;
A2:-(f|X) = (-1)(#)(f|X) by VFUNCT_1:23;
hence -(f|X) is Lipschitzian by A1;
thus (-f)|X is Lipschitzian by A1,A2,VFUNCT_1:29;
(||.f.||)|X = ||. f|X .|| by VFUNCT_1:29;
hence thesis by A1;
end;
registration let S;
cluster constant -> 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<r and
A2: for x1,x2 st x1 in X & x2 in X
holds ||.f/.x1-f/.x2 .||<=r*|.x1-x2.|;
now let x0 such that A3: x0 in X;
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
let g be Real such that A4: 0<g;
set s=g/r;
take s9=s;
A5: now let x1;
assume that
A6: x1 in dom f and
A7: |.x1-x0.|<s;
r*|.x1-x0.|<(g/r)*r by A1,A7,XREAL_1:68; then
A8: r*|.x1-x0.|<g by A1,XCMPLX_1:87;
||. f/.x1 - f/.x0 .||<=r*|.x1-x0.| by A2,A3,A6;
hence ||. f/.x1 - f/.x0 .||<g by A8,XXREAL_0:2;
end;
s9=g*r" by XCMPLX_0:def 9;
hence thesis by A1,A4,A5,XREAL_1:129;
end;
hence f is_continuous_in x0 by A3,Th8;
end;
hence thesis;
end;
end;
theorem
(ex r be Point of S st rng f = {r}) implies f is continuous
proof
given r be Point of S such that A1: rng f = {r};
now
let x1,x2;
assume A2: x1 in dom f & x2 in dom f; then
f.x2 in rng f by FUNCT_1:def 3; then
f/.x2 in rng f by A2,PARTFUN1:def 6; then
A3: f/.x2=r by A1,TARSKI:def 1;
f.x1 in rng f by A2,FUNCT_1:def 3; then
f/.x1 in rng f by A2,PARTFUN1:def 6; then
f/.x1=r by A1,TARSKI:def 1; then
||.f/.x1-f/.x2 .|| = 0 by A3,NORMSP_1:6;
hence ||. f/.x1-f/.x2 .|| <= 1*|.x1-x2.| by COMPLEX1:46;
end; then
f is Lipschitzian;
hence thesis;
end;
theorem
for r, p be Point of S st (for x0 st x0 in X holds f/.x0 = x0*r+p)
holds f|X is continuous
proof
let r, p be Point of S;
assume A1: for x0 st x0 in X holds f/.x0 = x0*r+p;
A2:now let x1,x2;
assume A3: x1 in dom(f|X) & x2 in dom(f|X); then
x2 in X; then
A4: f/.x2 = x2*r+p by A1;
A5: 0<=|.x1-x2.| by COMPLEX1:46;
x1 in X by A3; then
f/.x1 = x1*r+p by A1; then
||. f/.x1-f/.x2.|| = ||. x1*r+(p-(p+x2*r)).|| by A4,RLVECT_1:def 3
.= ||. x1*r+(p-p-x2*r).|| by RLVECT_1:27
.= ||. x1*r+(0.S-x2*r).|| by RLVECT_1:15
.= ||. x1*r-x2*r.|| by RLVECT_1:14
.= ||. (x1-x2)*r.|| by RLVECT_1:35
.= |.x1-x2.|* ||. r .|| by NORMSP_1:def 1; then
||.f/.x1-f/.x2.|| + (0 qua Nat) <= ||.r.||*|.x1-x2.| + 1*|.x1-x2.|
by A5,XREAL_1:7;
hence ||.f/.x1-f/.x2.|| <= (||.r.||+1)*|.x1-x2.|;
end;
(0 qua Nat)+(0 qua Nat) < ||.r.|| +1 by NORMSP_1:4,XREAL_1:8; then
f|X is Lipschitzian by A2,Th26;
hence thesis;
end;