:: The Continuous Functions on Normed Linear Spaces
:: by Takaya Nishiyama, Keiji Ohkubo and Yasunari Shidama
::
:: Received April 6, 2004
:: Copyright (c) 2004-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, REAL_1, NORMSP_1, PARTFUN1, NAT_1, PRE_TOPC,
XBOOLE_0, ALGSTR_0, ARYTM_1, ARYTM_3, FUNCT_1, RELAT_1, STRUCT_0,
RCOMP_1, CARD_1, TARSKI, XXREAL_0, SUPINF_2, VALUED_0, SEQ_2, ORDINAL2,
FCONT_1, FUNCT_2, COMPLEX1, VALUED_1, CFCONT_1, SEQ_1, SEQ_4, NFCONT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
PARTFUN2, FUNCT_2, PRE_TOPC, VALUED_0, STRUCT_0, ALGSTR_0, ORDINAL1,
NUMBERS, XCMPLX_0, COMPLEX1, REAL_1, XREAL_0, RLVECT_1, SEQ_1, SEQ_2,
SEQ_4, RCOMP_1, VFUNCT_1, NORMSP_0, NORMSP_1, XXREAL_0;
constructors REAL_1, COMPLEX1, SEQ_2, SEQ_4, RCOMP_1, PARTFUN2, VFUNCT_1,
RELSET_1, COMSEQ_2;
registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, NAT_1, STRUCT_0,
RLVECT_1, VALUED_0, XREAL_0, VFUNCT_1, FUNCT_2;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions TARSKI;
equalities RLVECT_1, RELAT_1;
expansions TARSKI;
theorems TARSKI, XBOOLE_0, XBOOLE_1, RLVECT_1, XCMPLX_0, XCMPLX_1, ZFMISC_1,
RCOMP_1, SEQ_2, RELAT_1, FUNCT_1, VFUNCT_1, LOPBAN_1, FUNCT_2, SEQ_4,
NORMSP_1, PARTFUN1, PARTFUN2, XREAL_1, COMPLEX1, XXREAL_0, BHSP_1,
VALUED_0, NORMSP_0, ORDINAL1;
schemes FUNCT_2;
begin :: Continuous Functions on Normed Linear Spaces
reserve n,m for Nat;
reserve x,X,X1 for set;
reserve s,g,r,p for Real;
reserve S,T for RealNormSpace;
reserve f,f1,f2 for PartFunc of S,T;
reserve s1,s2 for sequence of S;
reserve x0,x1,x2 for Point of S;
reserve Y for Subset of S;
theorem
for S being non empty addLoopStr for seq1,seq2 be sequence of S holds
seq1 - seq2 = seq1 +- seq2
proof
let S be non empty addLoopStr;
let seq1, seq2 be sequence of S;
for n being Element of NAT holds (seq1 - seq2).n = (seq1 +- seq2).n
proof
let n be Element of NAT;
thus (seq1 - seq2).n = seq1.n - seq2.n by NORMSP_1:def 3
.= seq1.n + (-seq2).n by BHSP_1:44
.= (seq1+-seq2).n by NORMSP_1:def 2;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th2:
for seq be sequence of S holds -seq=(-1)*seq
proof
let seq be sequence of S;
now
let n be Element of NAT;
thus ((-1)*seq).n =(-1)*seq.n by NORMSP_1:def 5
.=-seq.n by RLVECT_1:16
.=(-seq).n by BHSP_1:44;
end;
hence thesis by FUNCT_2:63;
end;
definition
let S, x0;
mode Neighbourhood of x0 -> Subset of S means
:Def1:
ex g be Real
st 0<g & { y where y is Point of S: ||.y-x0 .|| < g} c= it;
existence
proof
set N= {y where y is Point of S : ||.y-x0 .|| < 1};
take N;
N c= the carrier of S
proof
let x be object;
assume x in {y where y is Point of S : ||.y-x0 .|| < 1};
then ex y be Point of S st x=y & ||.y-x0 .|| < 1;
hence thesis;
end;
hence thesis;
end;
end;
theorem Th3:
for g be Real st 0<g holds
{y where y is Point of S: ||.y-x0 .|| < g} is Neighbourhood of x0
proof
let g be Real such that
A1: g >0;
set N= {y where y is Point of S : ||.y-x0 .|| < g};
N c= the carrier of S
proof
let x be object;
assume x in {y where y is Point of S : ||.y-x0 .|| < g};
then ex y be Point of S st x=y & ||.y-x0 .|| < g;
hence thesis;
end;
hence thesis by A1,Def1;
end;
theorem Th4:
for N being Neighbourhood of x0 holds x0 in N
proof
let N be Neighbourhood of x0;
consider g be Real such that
A1: 0<g and
A2: {z where z is Point of S : ||.z-x0 .|| < g} c= N by Def1;
||.x0-x0 .|| = ||.0.S.|| by RLVECT_1:15
.=0 by NORMSP_1:1;
then x0 in {z where z is Point of S : ||.z-x0 .|| < g} by A1;
hence thesis by A2;
end;
definition
let S;
let X be Subset of S;
attr X is compact means
for s1 be sequence of S st rng s1 c= X
ex s2 be sequence of S st s2 is subsequence of s1 & s2 is convergent &
lim s2 in X;
end;
definition
let S;
let X be Subset of S;
attr X is closed means
for s1 be sequence of S st rng s1 c= X & s1 is convergent holds lim s1 in X;
end;
definition
let S;
let X be Subset of S;
attr X is open means
X` is closed;
end;
definition
let S,T;
let 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;
definition
let S;
let f be PartFunc of the carrier of S,REAL;
let 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 Th5:
for seq be sequence of S, h be PartFunc of S,T st rng seq c= dom h holds
seq.n in dom h
proof
let seq be sequence of S;
A1: n in NAT by ORDINAL1:def 12;
dom seq = NAT by FUNCT_2:def 1;
then seq.n in rng seq by FUNCT_1:def 3,A1;
hence thesis;
end;
theorem Th6:
for seq be sequence of S, x be set holds x in rng seq iff ex n st x = seq.n
proof
let seq be sequence of S;
let x be set;
thus x in rng seq implies ex n st x = seq.n
proof
assume x in rng seq;
then consider y be object such that
A1: y in dom seq and
A2: x = seq.y by FUNCT_1:def 3;
reconsider m=y as Nat by A1;
take m;
thus thesis by A2;
end;
given n such that
A3: x = seq.n;
n in NAT by ORDINAL1:def 12;
then n in dom seq by FUNCT_2:def 1;
hence thesis by A3,FUNCT_1:def 3;
end;
theorem Th7:
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;
reconsider r as Real;
defpred P[Nat ,Point of S] 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 be Point of S 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 p be Point of S such that
A5: p in dom f & ||.p-x0 .|| < 1/(n+1) & not ||.f/.p-f/.x0 .|| <r by A3;
take p;
thus thesis by A5;
end;
consider s1 being sequence of S such that
A6: for n being Element of NAT holds P[n,s1.n] from FUNCT_2:sch 3(A4);
reconsider s1 as sequence of S;
A7: rng s1 c= dom f
proof
A8: dom s1= NAT by FUNCT_2:def 1;
let v be object;
assume v in rng s1;
then ex n be object st n in NAT & v=s1.n by A8,FUNCT_1:def 3;
hence thesis by A6;
end;
A9: now
let n;
A10: n in NAT by ORDINAL1:def 12;
not ||.f/.(s1.n)-f/.x0 .||<r by A6,A10;
hence not ||.(f/*s1).n-f/.x0 .||<r by A7,FUNCT_2:109,A10;
end;
A11: now
let s be Real;
consider n being Nat such that
A12: s"<n by SEQ_4:3;
assume 0<s;
then
A13: 0<s";
s"+0 <n+1 by A12,XREAL_1:8;
then 1/(n+1)<1/s" by A13,XREAL_1:76;
then
A14: 1/(n+1)<s by XCMPLX_1:216;
take k=n;
let m be Nat;
A15: 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 A14,XXREAL_0:2;
hence ||. s1.m-x0 .|| <s by A6,XXREAL_0:2,A15;
end;
then
A16: s1 is convergent by NORMSP_1:def 6;
then lim s1=x0 by A11,NORMSP_1:def 7;
then f/*s1 is convergent & f/.x0=lim(f/*s1) by A1,A7,A16;
then consider n being Nat such that
A17: for m being Nat st n<=m holds ||.(f/*s1).m-f/.x0.||<r
by A2,NORMSP_1:def 7;
||.(f/*s1).n-f/.x0.||<r by A17;
hence contradiction by A9;
end;
assume that
A18: x0 in dom f and
A19: 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
A20: rng s1 c= dom f and
A21: s1 is convergent & lim s1 = x0;
A22: now
let p be Real;
assume 0<p;
then consider s such that
A23: 0<s and
A24: for x1 st x1 in dom f & ||. x1- x0 .|| <s holds ||. f/.x1- f/.
x0 .|| <p by A19;
reconsider s as Real;
consider n being Nat such that
A25: for m being Nat st n<=m holds ||. s1.m-x0 .|| <s
by A21,A23,NORMSP_1:def 7;
take k=n;
let m be Nat;
assume k<=m;
then
A26: ||. s1.m-x0 .|| <s by A25;
A27: m in NAT by ORDINAL1:def 12;
dom s1 = NAT by FUNCT_2:def 1;
then s1.m in rng s1 by FUNCT_1:3,A27;
then ||.f/.(s1.m)-f/.x0.||<p by A20,A24,A26;
hence ||.(f/*s1).m - f/.x0.||<p by A20,FUNCT_2:109,A27;
end;
then f/*s1 is convergent by NORMSP_1:def 6;
hence f/*s1 is convergent & f/.x0 = lim (f/*s1) by A22,NORMSP_1:def 7;
end;
hence thesis by A18;
end;
theorem Th8:
for f be PartFunc of the carrier of S,REAL holds (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
let f be PartFunc of the carrier of S,REAL;
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 ,Point of S] 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 be Point of S 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 p be Point of S such that
A5: p in dom f & ||.p-x0 .|| < 1/(n+1) & |.f/.p-f/.x0 .| >= r by A3;
take p;
thus thesis by A5;
end;
consider s1 being sequence of S such that
A6: for n being Element of NAT holds P[n,s1.n] from FUNCT_2:sch 3(A4);
reconsider s1 as sequence of S;
A7: rng s1 c= dom f
proof
A8: dom s1= NAT by FUNCT_2:def 1;
let v be object;
assume v in rng s1;
then ex n be object st n in NAT & v=s1.n by A8,FUNCT_1:def 3;
hence thesis by A6;
end;
A9: now
let n;
A10: n in NAT by ORDINAL1:def 12;
|.f/.(s1.n)-f/.x0 .|>=r by A6,A10;
hence |. (f/*s1).n-f/.x0 .| >= r by A7,FUNCT_2:109,A10;
end;
A11: now
let s be Real;
consider n being Nat such that
A12: s"<n by SEQ_4:3;
assume 0<s;
then
A13: 0<s";
s"+0 <n+1 by A12,XREAL_1:8;
then 1/(n+1)<1/s" by A13,XREAL_1:76;
then
A14: 1/(n+1)<s by XCMPLX_1:216;
take k=n;
let m be Nat;
A15: 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 A14,XXREAL_0:2;
hence ||. s1.m-x0 .|| <s by A6,XXREAL_0:2,A15;
end;
then
A16: s1 is convergent by NORMSP_1:def 6;
then lim s1=x0 by A11,NORMSP_1:def 7;
then f/*s1 is convergent & f/.x0=lim(f/*s1) by A1,A7,A16;
then consider n being Nat such that
A17: for m being Nat st n<=m holds |. (f/*s1).m-f/.x0.|<r by A2,SEQ_2:def 7;
|.(f/*s1).n-f/.x0.| <r by A17;
hence contradiction by A9;
end;
assume that
A18: x0 in dom f and
A19: 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
A20: rng s1 c= dom f and
A21: s1 is convergent & lim s1 = x0;
A22: now
let p be Real;
reconsider pp=p as Real;
assume 0<p;
then consider s such that
A23: 0<s and
A24: for x1 st x1 in dom f & ||. x1- x0 .|| <s holds |. f/.x1- f/.
x0 .| <pp by A19;
reconsider s as Real;
consider n being Nat such that
A25: for m being Nat st n<=m holds ||. s1.m-x0 .|| <s
by A21,A23,NORMSP_1:def 7;
take k=n;
let m be Nat;
A26: m in NAT by ORDINAL1:def 12;
assume k<=m;
then
A27: ||. s1.m-x0 .|| <s by A25;
dom s1 = NAT by FUNCT_2:def 1;
then s1.m in rng s1 by FUNCT_1:3,A26;
then |.f/.(s1.m)-f/.x0.| <p by A20,A24,A27;
hence |. (f/*s1).m - f/.x0.| <p by A20,FUNCT_2:109,A26;
end;
then f/*s1 is convergent by SEQ_2:def 6;
hence f/*s1 is convergent & f/.x0 = lim (f/*s1) by A22,SEQ_2:def 7;
end;
hence thesis by A18;
end;
theorem Th9:
for 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 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 N1 be Neighbourhood of f/.x0;
consider r such that
A2: 0<r and
A3: {y where y is Point of T : ||.y-f/.x0 .|| < r} c= N1 by Def1;
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,Th7;
reconsider s as Real;
reconsider N={z where z is Point of S : ||.z-x0 .|| < s} as Neighbourhood
of x0 by A4,Th3;
take N;
let x1;
assume that
A6: x1 in dom f and
A7: x1 in N;
ex z be Point of S st x1=z & ||.z-x0 .|| < s by A7;
then ||. f/.x1- f/.x0 .|| <r by A5,A6;
then f/.x1 in {y where y is Point of T : ||.y-f/.x0 .|| < r};
hence thesis by A3;
end;
assume that
A8: x0 in dom f and
A9: 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
A10: 0<r;
reconsider rr=r as Real;
reconsider N1 = {y where y is Point of T : ||.y-f/.x0 .|| < rr} as
Neighbourhood of f/.x0 by Th3,A10;
consider N2 being Neighbourhood of x0 such that
A11: for x1 st x1 in dom f & x1 in N2 holds f/.x1 in N1 by A9;
consider s such that
A12: 0<s and
A13: {z where z is Point of S : ||.z-x0 .|| < s} c= N2 by Def1;
take s;
for x1 st x1 in dom f & ||. x1- x0 .|| <s holds ||. f/.x1- f/.x0 .|| <r
proof
let x1;
assume that
A14: x1 in dom f and
A15: ||. x1- x0 .|| <s;
x1 in {z where z is Point of S : ||.z-x0 .|| < s} by A15;
then f/.x1 in N1 by A11,A13,A14;
then ex y be Point of T st f/.x1=y & ||.y-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 A12;
end;
hence thesis by A8,Th7;
end;
theorem Th10:
for 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 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 Point of S such that
A3: x in dom f and
A4: x in N and
A5: r=f.x by PARTFUN2:59;
r=f/.x by A3,A5,PARTFUN1:def 6;
hence r in N1 by A2,A3,A4;
end;
hence thesis;
end;
assume that
A6: x0 in dom f and
A7: 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
A8: f.:N c= N1 by A7;
take N;
let x1;
assume that
A9: x1 in dom f and
A10: x1 in N;
f.x1 in f.:N by A9,A10,FUNCT_1:def 6;
then f.x1 in N1 by A8;
hence f/.x1 in N1 by A9,PARTFUN1:def 6;
end;
hence thesis by A6,Th9;
end;
theorem
x0 in dom f & (ex N be Neighbourhood of x0 st dom f /\ N = {x0})
implies f is_continuous_in x0
proof
assume
A1: x0 in dom f;
given N be Neighbourhood of x0 such that
A2: dom f /\ N = {x0};
now
let N1 be Neighbourhood of f/.x0;
take N;
A3: f/.x0 in N1 by Th4;
f.:N = Im(f,x0) by A2,RELAT_1:112
.= {f.x0} by A1,FUNCT_1:59
.= {f/.x0} by A1,PARTFUN1:def 6;
hence f.:N c= N1 by A3,ZFMISC_1:31;
end;
hence thesis by A1,Th10;
end;
theorem Th12:
for h1,h2 be PartFunc of S,T for seq be sequence of S 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 S,T;
let seq be sequence of S;
A1: dom h1 /\ dom h2 c= dom h1 by XBOOLE_1:17;
A2: dom h1 /\ dom h2 c= dom h2 by XBOOLE_1:17;
assume
A3: rng seq c= dom h1 /\ dom h2;
then
A4: rng seq c= dom (h1 + h2) by VFUNCT_1:def 1;
now
let n be Nat;
A5: n in NAT by ORDINAL1:def 12;
A6: seq.n in dom (h1 + h2) by A4,Th5;
thus ((h1+h2)/*seq).n = (h1+h2)/.(seq.n) by A4,FUNCT_2:109,A5
.= h1/.(seq.n) + h2/.(seq.n) by A6,VFUNCT_1:def 1
.= (h1/*seq).n + h2/.(seq.n) by A3,A1,FUNCT_2:109,XBOOLE_1:1,A5
.= (h1/*seq).n + (h2/*seq).n by A3,A2,FUNCT_2:109,XBOOLE_1:1,A5;
end;
hence (h1+h2)/*seq=h1/*seq+h2/*seq by NORMSP_1:def 2;
A7: rng seq c= dom (h1 - h2) by A3,VFUNCT_1:def 2;
now
let n be Nat;
A8: n in NAT by ORDINAL1:def 12;
A9: seq.n in dom (h1 - h2) by A7,Th5;
thus ((h1-h2)/*seq).n = (h1-h2)/.(seq.n) by A7,FUNCT_2:109,A8
.= h1/.(seq.n) - h2/.(seq.n) by A9,VFUNCT_1:def 2
.= (h1/*seq).n - h2/.(seq.n) by A3,A1,FUNCT_2:109,XBOOLE_1:1,A8
.= (h1/*seq).n - (h2/*seq).n by A3,A2,FUNCT_2:109,XBOOLE_1:1,A8;
end;
hence thesis by NORMSP_1:def 3;
end;
theorem Th13:
for h be PartFunc of S,T for seq be sequence of S
for r be Real
st rng seq c= dom h holds (r(#)h)/*seq = r*(h/*seq)
proof
let h be PartFunc of S,T;
let seq be sequence of S;
let 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 be Nat;
A3: n in NAT by ORDINAL1:def 12;
A4: seq.n in dom (r(#)h) by A2,Th5;
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;
reconsider jj=1 as Real;
theorem Th14:
for h be PartFunc of S,T for seq be sequence of S st rng seq c=
dom h holds ||.h/*seq .|| = ||.h.||/*seq & -(h/*seq) = (-h)/*seq
proof
let h be PartFunc of S,T;
let seq be sequence of S;
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 Th6;
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;
thus -(h/*seq) =(-jj)*(h/*seq) by Th2
.= ((-1)(#)h)/*seq by A1,Th13
.= (-h)/*seq by VFUNCT_1:23;
end;
theorem
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 that
A1: f1 is_continuous_in x0 and
A2: f2 is_continuous_in x0;
A3: x0 in dom f1 & x0 in dom f2 by A1,A2;
now
x0 in dom f1 /\ dom f2 by A3,XBOOLE_0:def 4;
hence
A4: x0 in dom (f1+f2) by VFUNCT_1:def 1;
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) = dom f1 /\ dom f2 by VFUNCT_1:def 1;
then dom (f1+f2) c= dom f2 by XBOOLE_1:17;
then
A8: rng s1 c= dom f2 by A5;
then
A9: f2/*s1 is convergent by A2,A6;
dom (f1+f2) = dom f1 /\ dom f2 by VFUNCT_1:def 1;
then dom (f1+f2) c= dom f1 by XBOOLE_1:17;
then
A10: rng s1 c= dom f1 by A5;
then
A11: f1/*s1 is convergent by A1,A6;
then (f1/*s1)+(f2/*s1) is convergent by A9,NORMSP_1:19;
hence (f1+f2)/*s1 is convergent by A7,Th12;
A12: f1/.x0 = lim (f1/*s1) by A1,A6,A10;
A13: 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 A11,A12,A9,A13,NORMSP_1:25
.= lim ((f1+f2)/*s1) by A7,Th12;
end;
hence f1+f2 is_continuous_in x0;
now
x0 in dom f1 /\ dom f2 by A3,XBOOLE_0:def 4;
hence
A14: x0 in dom (f1-f2) by VFUNCT_1:def 2;
let s1;
assume that
A15: rng s1 c= dom(f1-f2) and
A16: s1 is convergent & lim s1=x0;
A17: rng s1 c= dom f1 /\ dom f2 by A15,VFUNCT_1:def 2;
dom (f1-f2) = dom f1 /\ dom f2 by VFUNCT_1:def 2;
then dom (f1-f2) c= dom f2 by XBOOLE_1:17;
then
A18: rng s1 c= dom f2 by A15;
then
A19: f2/*s1 is convergent by A2,A16;
dom (f1-f2) = dom f1 /\ dom f2 by VFUNCT_1:def 2;
then dom (f1-f2) c= dom f1 by XBOOLE_1:17;
then
A20: rng s1 c= dom f1 by A15;
then
A21: f1/*s1 is convergent by A1,A16;
then f1/*s1-f2/*s1 is convergent by A19,NORMSP_1:20;
hence (f1-f2)/*s1 is convergent by A17,Th12;
A22: f1/.x0 = lim (f1/*s1) by A1,A16,A20;
A23: f2/.x0 = lim (f2/*s1) by A2,A16,A18;
thus (f1-f2)/.x0 = f1/.x0 - f2/.x0 by A14,VFUNCT_1:def 2
.= lim (f1/*s1 - f2/*s1) by A21,A22,A19,A23,NORMSP_1:26
.= lim ((f1-f2)/*s1) by A17,Th12;
end;
hence thesis;
end;
theorem Th16:
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;
reconsider rr=r as Real;
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,Th13;
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,Th13;
end;
theorem
f is_continuous_in x0 implies ||. f .|| is_continuous_in x0 & -f
is_continuous_in x0
proof
assume
A1: f is_continuous_in x0;
then
A2: x0 in dom f;
now
thus
A3: x0 in dom (||.f .||) by A2,NORMSP_0:def 3;
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 A1,A5;
A8: f/*s1 is convergent by A1,A5,A6;
then ||.f/*s1.|| is convergent by NORMSP_1:23;
hence ||.f.||/*s1 is convergent by A6,Th14;
thus ||.f.||/.x0 =||.f.||.x0 by A3,PARTFUN1:def 6
.= ||.f/.x0 .|| by A3,NORMSP_0:def 3
.= lim ||.f/*s1 .|| by A8,A7,LOPBAN_1:41
.= lim (||.f.||/*s1) by A6,Th14;
end;
hence ||.f .|| is_continuous_in x0;
-f=(-1)(#)f by VFUNCT_1:23;
hence thesis by A1,Th16;
end;
definition
let S,T;
let f,X;
pred f is_continuous_on X means
X c= dom f & for x0 st x0 in X holds f|X is_continuous_in x0;
end;
definition
let S;
let f be PartFunc of the carrier of S, REAL;
let X;
pred f is_continuous_on X means
X c= dom f & for x0 st x0 in X holds f|X is_continuous_in x0;
end;
theorem Th18:
for X,f holds f is_continuous_on X iff X c= dom f & 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;
thus f is_continuous_on X implies X c= dom f & 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
A1: f is_continuous_on X;
then
A2: X c= dom f;
now
let s1 such that
A3: rng s1 c= X and
A4: s1 is convergent and
A5: lim s1 in X;
A6: f|X is_continuous_in (lim s1) by A1,A5;
A7: dom (f|X) = dom f /\ X by PARTFUN2:15
.= X by A2,XBOOLE_1:28;
now
let n be Element of NAT;
dom s1 = NAT by FUNCT_2:def 1;
then
A8: s1.n in rng s1 by FUNCT_1:3;
thus ((f|X)/*s1).n = (f|X)/.(s1.n) by A3,A7,FUNCT_2:109
.= f/.(s1.n) by A3,A7,A8,PARTFUN2:15
.= (f/*s1).n by A2,A3,FUNCT_2:109,XBOOLE_1:1;
end;
then
A9: (f|X)/*s1 = f/*s1 by FUNCT_2:63;
f/.(lim s1) = (f|X)/.(lim s1) by A5,A7,PARTFUN2:15
.= lim (f/*s1) by A3,A4,A7,A6,A9;
hence
f/*s1 is convergent & f/.(lim s1) = lim (f/*s1) by A3,A4,A7,A6,A9;
end;
hence thesis by A1;
end;
assume that
A10: X c= dom f and
A11: 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
A12: dom (f|X) = dom f /\ X by PARTFUN2:15
.= X by A10,XBOOLE_1:28;
let x1 such that
A13: x1 in X;
now
let s1 such that
A14: rng s1 c= dom (f|X) and
A15: s1 is convergent and
A16: lim s1=x1;
now
let n be Element of NAT;
dom s1 = NAT by FUNCT_2:def 1;
then
A17: s1.n in rng s1 by FUNCT_1:3;
thus ((f|X)/*s1).n = (f|X)/.(s1.n) by A14,FUNCT_2:109
.= f/.(s1.n) by A14,A17,PARTFUN2:15
.= (f/*s1).n by A10,A12,A14,FUNCT_2:109,XBOOLE_1:1;
end;
then
A18: (f|X)/*s1 = f/*s1 by FUNCT_2:63;
(f|X)/.(lim s1) = f/.(lim s1) by A13,A12,A16,PARTFUN2:15
.= lim ((f|X)/*s1) by A11,A13,A12,A14,A15,A16,A18;
hence (f|X)/*s1 is convergent & (f|X)/.x1 = lim ((f|X)/*s1) by A11,A13
,A12,A14,A15,A16,A18;
end;
hence f|X is_continuous_in x1 by A13,A12;
end;
hence thesis by A10;
end;
theorem Th19:
f is_continuous_on X iff X c= dom f & 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
thus f is_continuous_on X implies X c= dom f & 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: f is_continuous_on X;
hence X c= dom f;
A2: X c= dom f by A1;
let x0,r;
assume that
A3: x0 in X and
A4: 0<r;
f|X is_continuous_in x0 by A1,A3;
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,Th7;
take s;
thus 0<s by A5;
let x1;
assume that
A7: x1 in X and
A8: ||. x1- x0 .|| <s;
A9: dom (f|X) = dom f /\ X by PARTFUN2:15
.= X by A2,XBOOLE_1:28;
then ||. f/.x1 - f/.x0 .|| = ||. (f|X)/.x1 - f/.x0 .|| by A7,PARTFUN2:15
.= ||. (f|X)/.x1 - (f|X)/.x0 .|| by A3,A9,PARTFUN2:15;
hence thesis by A6,A9,A7,A8;
end;
assume that
A10: X c= dom f and
A11: 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;
A12: dom (f|X) = dom f /\ X by PARTFUN2:15
.= X by A10,XBOOLE_1:28;
now
let x0 such that
A13: 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
A14: 0<s and
A15: for x1 st x1 in X & ||. x1- x0 .|| < s holds ||. f/.x1 - f/.x0
.|| < r by A11,A13;
take s;
thus 0<s by A14;
let x1 such that
A16: x1 in dom(f|X) and
A17: ||. x1- x0 .|| <s;
||. (f|X)/.x1-(f|X)/.x0.|| = ||. (f|X)/.x1 - f/.x0.|| by A12,A13,
PARTFUN2:15
.= ||. f/.x1 - f/.x0 .|| by A16,PARTFUN2:15;
hence thesis by A12,A15,A16,A17;
end;
hence f|X is_continuous_in x0 by A12,A13,Th7;
end;
hence thesis by A10;
end;
theorem
for f be PartFunc of the carrier of S, REAL holds ( f is_continuous_on
X iff X c= dom f & 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
let f be PartFunc of the carrier of S, REAL;
thus f is_continuous_on X implies X c= dom f & 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: f is_continuous_on X;
hence X c= dom f;
A2: X c= dom f by A1;
let x0,r;
assume that
A3: x0 in X and
A4: 0<r;
f|X is_continuous_in x0 by A1,A3;
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: dom (f|X) = dom f /\ X by PARTFUN2:15
.= X by A2,XBOOLE_1:28;
then |. f/.x1 - f/.x0 .| = |. (f|X)/.x1 - f/.x0 .| by A7,PARTFUN2:15
.= |. (f|X)/.x1 - (f|X)/.x0 .| by A3,A9,PARTFUN2:15;
hence thesis by A6,A9,A7,A8;
end;
assume that
A10: X c= dom f and
A11: 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;
A12: dom (f|X) = dom f /\ X by PARTFUN2:15
.= X by A10,XBOOLE_1:28;
now
let x0 such that
A13: 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
A14: 0<s and
A15: for x1 st x1 in X & ||. x1- x0 .|| < s holds |. f/.x1 - f/.x0
.| < r by A11,A13;
take s;
thus 0<s by A14;
let x1 such that
A16: x1 in dom(f|X) and
A17: ||. x1- x0 .|| <s;
|. (f|X)/.x1-(f|X)/.x0 .| = |. (f|X)/.x1 - f/.x0 .| by A12,A13,
PARTFUN2:15
.= |. f/.x1 - f/.x0 .| by A16,PARTFUN2:15;
hence thesis by A12,A15,A16,A17;
end;
hence f|X is_continuous_in x0 by A12,A13,Th8;
end;
hence thesis by A10;
end;
theorem
f is_continuous_on X iff f|X is_continuous_on X
proof
thus f is_continuous_on X implies f|X is_continuous_on X
proof
assume
A1: f is_continuous_on X;
then X c= dom f;
then X c= dom f /\ X by XBOOLE_1:28;
hence X c= dom (f|X) by RELAT_1:61;
let r be Point of S;
assume r in X;
then f|X is_continuous_in r by A1;
hence thesis by RELAT_1:72;
end;
assume
A2: f|X is_continuous_on X;
then X c= dom(f|X);
then dom f /\ X c= dom f & X c= dom f /\ X by RELAT_1:61,XBOOLE_1:17;
hence X c= dom f;
let r be Point of S;
assume r in X;
then (f|X)|X is_continuous_in r by A2;
hence thesis by RELAT_1:72;
end;
theorem Th22:
for f be PartFunc of the carrier of S,REAL holds (f
is_continuous_on X iff f|X is_continuous_on X)
proof
let f be PartFunc of the carrier of S,REAL;
thus f is_continuous_on X implies f|X is_continuous_on X
proof
assume
A1: f is_continuous_on X;
then X c= dom f;
then X c= dom f /\ X by XBOOLE_1:28;
hence X c= dom (f|X) by RELAT_1:61;
let r be Point of S;
assume r in X;
then f|X is_continuous_in r by A1;
hence thesis by RELAT_1:72;
end;
assume
A2: f|X is_continuous_on X;
then X c= dom(f|X);
then dom f /\ X c= dom f & X c= dom f /\ X by RELAT_1:61,XBOOLE_1:17;
hence X c= dom f;
let r be Point of S;
assume r in X;
then (f|X)|X is_continuous_in r by A2;
hence thesis by RELAT_1:72;
end;
theorem Th23:
f is_continuous_on X & X1 c= X implies f is_continuous_on X1
proof
assume that
A1: f is_continuous_on X and
A2: X1 c= X;
X c= dom f by A1;
hence
A3: X1 c= dom f by A2;
let r be Point of S;
assume
A4: r in X1;
then
A5: f|X is_continuous_in r by A1,A2;
thus f|X1 is_continuous_in r
proof
dom f /\ X1 c= dom f /\ X by A2,XBOOLE_1:26;
then dom (f|X1) c= dom f /\ X by RELAT_1:61;
then
A6: dom (f|X1) c= dom (f|X) by RELAT_1:61;
r in dom f /\ X1 by A3,A4,XBOOLE_0:def 4;
hence
A7: r in dom (f|X1) by RELAT_1:61;
then
A8: (f|X)/.r = f/.r by A6,PARTFUN2:15
.= (f|X1)/.r by A7,PARTFUN2:15;
let s1 such that
A9: rng s1 c= dom (f|X1) and
A10: s1 is convergent & lim s1 = r;
A11: rng s1 c= dom (f|X) by A9,A6;
A12: now
let n be Element of NAT;
dom s1 = NAT by FUNCT_2:def 1;
then
A13: s1.n in rng s1 by FUNCT_1:3;
thus ((f|X)/*s1).n = (f|X)/.(s1.n) by A9,A6,FUNCT_2:109,XBOOLE_1:1
.= f/.(s1.n) by A11,A13,PARTFUN2:15
.= (f|X1)/.(s1.n) by A9,A13,PARTFUN2:15
.= ((f|X1)/*s1).n by A9,FUNCT_2:109;
end;
(f|X)/*s1 is convergent & (f|X)/.r = lim ((f|X)/*s1) by A5,A10,A11;
hence thesis by A8,A12,FUNCT_2:63;
end;
end;
theorem
x0 in dom f implies f is_continuous_on {x0}
proof
assume
A1: x0 in dom f;
thus {x0} c= dom f
by A1,TARSKI:def 1;
let p be Point of S such that
A2: p in {x0};
thus f|{x0} is_continuous_in p
proof
p in dom f by A1,A2,TARSKI:def 1;
then p in dom f /\ {x0} by A2,XBOOLE_0:def 4;
hence p in dom (f|{x0}) by RELAT_1:61;
let s1;
assume that
A3: rng s1 c= dom(f|{x0}) and
s1 is convergent and
lim s1=p;
A4: dom f /\ {x0} c= {x0} by XBOOLE_1:17;
rng s1 c= dom f /\ {x0} by A3,RELAT_1:61;
then
A5: rng s1 c= {x0} by A4;
A6: now
let n;
A7: n in NAT by ORDINAL1:def 12;
dom s1 = NAT by FUNCT_2:def 1;
then s1.n in rng s1 by FUNCT_1:3,A7;
hence s1.n = x0 by A5,TARSKI:def 1;
end;
A8: p=x0 by A2,TARSKI:def 1;
A9: now
let g be Real such that
A10: 0<g;
reconsider n=0 as Nat;
take n;
let m being Nat such that
n<=m;
A11: m in NAT by ORDINAL1:def 12;
||. ((f|{x0})/*s1).m - (f|{x0})/.p.|| = ||. (f|{x0})/.(s1.m) - (f|{
x0})/.x0 .|| by A8,A3,FUNCT_2:109,A11
.= ||. (f|{x0})/.x0 - (f|{x0})/.x0.|| by A6
.= ||. 0.T .|| by RLVECT_1:15
.= 0 by NORMSP_1:1;
hence ||. ((f|{x0})/*s1).m - (f|{x0})/.p .|| < g by A10;
end;
hence (f|{x0})/*s1 is convergent by NORMSP_1:def 6;
hence thesis by A9,NORMSP_1:def 7;
end;
end;
theorem Th25:
for X,f1,f2 st f1 is_continuous_on X & f2 is_continuous_on X
holds f1+f2 is_continuous_on X & f1-f2 is_continuous_on X
proof
let X,f1,f2;
assume
A1: f1 is_continuous_on X & f2 is_continuous_on X;
then X c= dom f1 & X c= dom f2;
then
A2: X c= dom f1 /\ dom f2 by XBOOLE_1:19;
then
A3: X c= dom (f1+f2) by VFUNCT_1:def 1;
now
let s1;
assume that
A4: rng s1 c= X and
A5: s1 is convergent and
A6: lim s1 in X;
A7: f1/*s1 is convergent & f2/*s1 is convergent by A1,A4,A5,A6,Th18;
then
A8: (f1/*s1)+(f2/*s1) is convergent by NORMSP_1:19;
A9: rng s1 c= dom f1 /\ dom f2 by A2,A4;
f1/.(lim s1) = lim (f1/*s1) & f2/.(lim s1) = lim (f2/*s1) by A1,A4,A5,A6
,Th18;
then (f1+f2)/.(lim s1) = lim (f1/*s1) + lim (f2/*s1) by A3,A6,
VFUNCT_1:def 1
.= lim (f1/*s1 + f2/*s1) by A7,NORMSP_1:25
.= lim ((f1+f2)/*s1) by A9,Th12;
hence
(f1+f2)/*s1 is convergent & (f1+f2)/.(lim s1)=lim((f1+f2)/*s1) by A9,A8
,Th12;
end;
hence f1+f2 is_continuous_on X by A3,Th18;
A10: X c= dom (f1-f2) by A2,VFUNCT_1:def 2;
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 A1,A11,A12,A13,Th18;
then
A15: (f1/*s1)-(f2/*s1) is convergent by NORMSP_1:20;
A16: rng s1 c= dom f1 /\ dom f2 by A2,A11;
f1/.(lim s1) = lim (f1/*s1) & f2/.(lim s1) = lim (f2/*s1) by A1,A11,A12,A13
,Th18;
then (f1-f2)/.(lim s1) = lim (f1/*s1) - lim (f2/*s1) by A10,A13,
VFUNCT_1:def 2
.= lim (f1/*s1 - f2/*s1) by A14,NORMSP_1:26
.= lim ((f1-f2)/*s1) by A16,Th12;
hence
(f1-f2)/*s1 is convergent & (f1-f2)/.(lim s1)=lim((f1-f2)/*s1) by A16,A15
,Th12;
end;
hence thesis by A10,Th18;
end;
theorem
for X,X1,f1,f2 st f1 is_continuous_on X & f2 is_continuous_on X1 holds
f1+f2 is_continuous_on X /\ X1 & f1-f2 is_continuous_on X /\ X1
proof
let X,X1,f1,f2;
assume f1 is_continuous_on X & f2 is_continuous_on X1;
then f1 is_continuous_on X /\ X1 & f2 is_continuous_on X /\ X1 by Th23,
XBOOLE_1:17;
hence thesis by Th25;
end;
theorem Th27:
for r,X,f st f is_continuous_on X holds r(#)f is_continuous_on X
proof
let r,X,f;
assume
A1: f is_continuous_on X;
then
A2: X c= dom f;
then
A3: X c= dom(r(#)f) by VFUNCT_1:def 4;
now
let s1;
assume that
A4: rng s1 c= X and
A5: s1 is convergent and
A6: lim s1 in X;
A7: f/*s1 is convergent by A1,A4,A5,A6,Th18;
then
A8: r*(f/*s1) is convergent by NORMSP_1:22;
f/.(lim s1) = lim (f/*s1) by A1,A4,A5,A6,Th18;
then (r(#)f)/.(lim s1) = r * lim (f/*s1) by A3,A6,VFUNCT_1:def 4
.= lim (r*(f/*s1)) by A7,NORMSP_1:28
.= lim ((r(#)f)/*s1) by A2,A4,Th13,XBOOLE_1:1;
hence
(r(#)f)/*s1 is convergent & (r(#)f)/.(lim s1)=lim((r(#)f)/*s1) by A2,A4,A8
,Th13,XBOOLE_1:1;
end;
hence thesis by A3,Th18;
end;
theorem Th28:
f is_continuous_on X implies ||.f.|| is_continuous_on X & -f
is_continuous_on X
proof
assume
A1: f is_continuous_on X;
thus ||.f.|| is_continuous_on X
proof
A2: X c= dom f by A1;
hence
A3: X c= dom (||.f.|| ) by NORMSP_0:def 3;
let r be Point of S;
assume
A4: r in X;
then
A5: f|X is_continuous_in r by A1;
thus (||.f.|| )|X is_continuous_in r
proof
A6: r in dom (||.f.|| ) /\ X by A3,A4,XBOOLE_0:def 4;
hence r in dom ((||.f.|| )|X) by RELAT_1:61;
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;
then
A10: (f|X)/.r = lim ((f|X)/*s1) by A5,A8;
now
let n be Element of NAT;
dom s1 = NAT by FUNCT_2:def 1;
then
A11: s1.n in rng s1 by FUNCT_1:3;
then s1.n in dom (f|X) by A9;
then
A12: s1.n in dom f /\ X by RELAT_1:61;
then
A13: s1.n in X by XBOOLE_0:def 4;
s1.n in dom f by A12,XBOOLE_0:def 4;
then
A14: 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,A11,PARTFUN2:15
.=(||.f.|| ).(s1.n) by A14,NORMSP_0:def 3
.=((||.f.|| )|X).(s1.n) by A13,FUNCT_1:49
.=((||.f.|| )|X)/.(s1.n) by A7,A11,PARTFUN1:def 6
.=((||.f.|||X)/*s1).n by A7,FUNCT_2:109;
end;
then
A15: ||.(f|X)/*s1.|| = (||.f.|||X)/*s1 by FUNCT_2:63;
A16: (f|X)/*s1 is convergent by A5,A8,A9;
hence (||.f.|||X)/*s1 is convergent by A15,NORMSP_1:23;
||.(f|X)/.r.|| = ||.f/.r.|| by A2,A4,PARTFUN2:17
.= (||.f.|| ).r by A3,A4,NORMSP_0:def 3
.= (||.f.|| )/.r by A3,A4,PARTFUN1:def 6
.= ((||.f.|| )|X)/.r by A6,PARTFUN2:16;
hence thesis by A16,A10,A15,LOPBAN_1:20;
end;
end;
(-1)(#)f is_continuous_on X by A1,Th27;
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 is_continuous_on the carrier of S
proof
assume that
A1: f is total and
A2: for x1,x2 holds f/.(x1+x2) = f/.x1 + f/.x2;
A3: dom f = the carrier of S by A1,PARTFUN1:def 2;
given x0 such that
A4: f is_continuous_in x0;
f/.x0 + 0.T =f/.x0
.= f/.(x0+0.S)
.= f/.x0+f/.0.S by A2;
then
A5: f/.0.S = 0.T by RLVECT_1:8;
A6: now
let x1;
0.T = f/.(x1+-x1) by A5,RLVECT_1:5
.= f/.x1+f/.(-x1) by A2;
hence -(f/.x1)=f/.(-x1) by RLVECT_1:6;
end;
A7: now
let x1,x2;
thus f/.(x1-x2)= f/.x1 + f/.(-x2) by A2
.= f/.x1 - f/.x2 by A6;
end;
now
let x1;
let r be Real;
assume that
x1 in the carrier of S 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,Th7;
take s;
thus s>0 by A9;
let x2 such that
x2 in the carrier of S and
A11: ||. x2-x1 .||<s;
A12: y+x0 =x1-(x0-x0) by RLVECT_1:29
.=x1- 0.S by RLVECT_1:15
.=x1;
then
A13: ||.x2-y-x0.||=||.x2-x1.|| by RLVECT_1:27;
||.f/.x2-f/.x1.|| = ||.f/.x2-(f/.y+f/.x0).|| by A2,A12
.= ||.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,A13;
end;
hence thesis by A3,Th19;
end;
theorem Th30:
for f st dom f is compact & f is_continuous_on (dom f) holds (
rng f) is compact
proof
let f;
assume that
A1: dom f is compact and
A2: f is_continuous_on (dom f);
now
let s1 be sequence of T 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 be Point of S 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 Point of S 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 sequence of S 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 consider n such that
A7: x = q1.n by Th6;
n in NAT by ORDINAL1:def 12;
hence x in dom f by A6,A7;
end;
then
A8: rng q1 c= dom f;
then consider s2 such that
A9: s2 is subsequence of q1 and
A10: s2 is convergent and
A11: (lim s2) in dom f by A1;
take q2 = f/*s2;
rng s2 c= rng q1 by A9,VALUED_0:21;
then
A12: rng s2 c= dom f by A8;
now
let n be Element of NAT;
f/.(q1.n)=s1.n by A6;
hence (f/*q1).n= s1.n by A8,FUNCT_2:109;
end;
then
A13: f/*q1=s1 by FUNCT_2:63;
f|(dom f) is_continuous_in (lim s2) by A2,A11;
then
A14: f is_continuous_in (lim s2) by RELAT_1:68;
then f/.(lim s2) = lim (f/*s2) by A10,A12;
hence
q2 is subsequence of s1 & q2 is convergent & (lim q2) in rng f by A8,A13,A9
,A10,A14,A12,PARTFUN2:2,VALUED_0:22;
end;
hence thesis;
end;
theorem Th31:
for f be PartFunc of the carrier of S, REAL st dom f is compact
& f is_continuous_on dom f holds rng f is compact
proof
let f be PartFunc of the carrier of S, REAL;
assume that
A1: dom f is compact and
A2: f is_continuous_on dom f;
now
let s1 be Real_Sequence 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 be Point of S 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 Point of S 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 sequence of S 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 consider n such that
A7: x = q1.n by Th6;
n in NAT by ORDINAL1:def 12;
hence x in dom f by A6,A7;
end;
then
A8: rng q1 c= dom f;
then consider s2 such that
A9: s2 is subsequence of q1 and
A10: s2 is convergent and
A11: (lim s2) in dom f by A1;
take q2 = f/*s2;
rng s2 c= rng q1 by A9,VALUED_0:21;
then
A12: rng s2 c= dom f by A8;
now
let n be Element of NAT;
f/.(q1.n)=s1.n by A6;
hence (f/*q1).n= s1.n by A8,FUNCT_2:109;
end;
then
A13: f/*q1=s1 by FUNCT_2:63;
f|(dom f) is_continuous_in (lim s2) by A2,A11;
then
A14: f is_continuous_in (lim s2) by RELAT_1:68;
then f/.(lim s2) = lim (f/*s2) by A10,A12;
hence
q2 is subsequence of s1 & q2 is convergent & (lim q2) in rng f by A8,A13,A9
,A10,A14,A12,PARTFUN2:2,VALUED_0:22;
end;
hence thesis by RCOMP_1:def 3;
end;
theorem
Y c= dom f & Y is compact & f is_continuous_on Y implies (f.:Y) is compact
proof
assume that
A1: Y c= dom f and
A2: Y is compact and
A3: f is_continuous_on Y;
A4: dom (f|Y) = dom f /\ Y by RELAT_1:61
.= Y by A1,XBOOLE_1:28;
f|Y is_continuous_on Y
proof
thus Y c= dom (f|Y) by A4;
let r be Point of S;
assume r in Y;
then f|Y is_continuous_in r by A3;
hence thesis by RELAT_1:72;
end;
then rng (f|Y) is compact by A2,A4,Th30;
hence thesis by RELAT_1:115;
end;
theorem Th33:
for f be PartFunc of the carrier of S,REAL st dom f<>{} & (dom f
) is compact & f is_continuous_on (dom f) ex x1,x2 st x1 in dom f & x2 in dom f
& f/.x1 = upper_bound (rng f) & f/.x2 = lower_bound (rng f)
proof
let f be PartFunc of the carrier of S,REAL;
assume dom f <> {} & dom f is compact & f is_continuous_on (dom f);
then
A1: rng f <> {} & rng f is compact by Th31,RELAT_1:42;
then consider x being Element of S such that
A2: x in dom f & upper_bound (rng f) = f.x by PARTFUN1:3,RCOMP_1:14;
take x;
consider y being Element of S such that
A3: y in dom f & lower_bound (rng f ) = f.y by A1,PARTFUN1:3,RCOMP_1:14;
take y;
thus thesis by A2,A3,PARTFUN1:def 6;
end;
theorem Th34:
for f st dom f<>{} & (dom f) is compact & f is_continuous_on (
dom f) ex x1,x2 st x1 in dom f & x2 in dom f & ||.f.||/.x1 = upper_bound (rng
||.f.||) & ||.f.||/.x2 = lower_bound (rng ||.f.||)
proof
let f such that
A1: dom f <> {} and
A2: dom f is compact and
A3: f is_continuous_on (dom f);
A4: dom f = dom ||.f.|| by NORMSP_0:def 3;
dom ||.f.|| is compact by A2,NORMSP_0:def 3;
then
A5: rng ||.f.|| is compact by A3,A4,Th28,Th31;
A6: rng ||.f.|| <> {} by A1,A4,RELAT_1:42;
then consider x being Element of S such that
A7: x in dom ||.f.|| & upper_bound (rng ||.f.||) = ||.f.||.x by A5,PARTFUN1:3
,RCOMP_1:14;
consider y being Element of S such that
A8: y in dom ||.f.|| & lower_bound (rng ||.f.||) = ||.f.||.y by A6,A5,
PARTFUN1:3,RCOMP_1:14;
take x;
take y;
thus thesis by A7,A8,NORMSP_0:def 3,PARTFUN1:def 6;
end;
theorem Th35:
(||.f.||)|X = ||.(f|X).||
proof
A1: dom ((||.f.||)|X) = dom (||.f.||) /\ X by RELAT_1:61
.= dom f /\ X by NORMSP_0:def 3
.= dom (f|X) by RELAT_1:61
.= dom ( ||.(f|X).||) by NORMSP_0:def 3;
now
let c be Point of S;
assume
A2: c in dom ((||.f.||)|X);
then
A3: c in dom (f|X) by A1,NORMSP_0:def 3;
c in dom (||.f.||) /\ X by A2,RELAT_1:61;
then
A4: c in dom (||.f.||) by XBOOLE_0:def 4;
thus ((||.f.||)|X).c = (||.f.||).c by A2,FUNCT_1:47
.= ||.f/.c.|| by A4,NORMSP_0:def 3
.= ||.(f|X)/.c.|| by A3,PARTFUN2:15
.= ||.(f|X).||.c by A1,A2,NORMSP_0:def 3;
end;
hence thesis by A1,PARTFUN1:5;
end;
theorem
for f,Y st Y<>{} & Y c= dom f & Y is compact & f is_continuous_on Y ex
x1,x2 st x1 in Y & x2 in Y & ||.f.||/.x1 = upper_bound (||.f.||.:Y) & ||.f.||/.
x2 = lower_bound (||.f.||.:Y)
proof
let f,Y such that
A1: Y <> {} and
A2: Y c= dom f and
A3: Y is compact and
A4: f is_continuous_on Y;
A5: dom (f|Y) = dom f /\ Y by RELAT_1:61
.= Y by A2,XBOOLE_1:28;
f|Y is_continuous_on Y
proof
thus Y c= dom (f|Y) by A5;
let r be Point of S;
assume r in Y;
then f|Y is_continuous_in r by A4;
hence thesis by RELAT_1:72;
end;
then consider x1,x2 such that
A6: x1 in dom (f|Y) and
A7: x2 in dom (f|Y) and
A8: ||.(f|Y).||/.x1 = upper_bound (rng ||.(f|Y).||) & ||.(f|Y).||/.x2 =
lower_bound (rng ||.(f|Y).||) by A1,A3,A5,Th34;
A9: dom f = dom ||.f.|| by NORMSP_0:def 3;
take x1,x2;
thus x1 in Y & x2 in Y by A5,A6,A7;
A10: ||.f.||.:Y =rng ( ||.f.|| | Y) by RELAT_1:115
.=rng( ||.(f|Y).|| ) by Th35;
A11: x2 in dom ||.(f|Y).|| by A7,NORMSP_0:def 3;
then
A12: ||.(f|Y).||/.x2 =||.(f|Y).||.x2 by PARTFUN1:def 6
.=||. (f|Y)/.x2.|| by A11,NORMSP_0:def 3
.=||. f/.x2.|| by A7,PARTFUN2:15
.=||. f.||.x2 by A2,A5,A7,A9,NORMSP_0:def 3
.=||. f.||/.x2 by A2,A5,A7,A9,PARTFUN1:def 6;
A13: x1 in dom ||.(f|Y).|| by A6,NORMSP_0:def 3;
then ||.(f|Y).||/.x1 =||.(f|Y).||.x1 by PARTFUN1:def 6
.=||. (f|Y)/.x1.|| by A13,NORMSP_0:def 3
.=||. f/.x1.|| by A6,PARTFUN2:15
.=||. f.||.x1 by A2,A5,A6,A9,NORMSP_0:def 3
.=||. f.||/.x1 by A2,A5,A6,A9,PARTFUN1:def 6;
hence thesis by A8,A12,A10;
end;
theorem
for f be PartFunc of the carrier of S,REAL for Y st Y<>{} & Y c= dom f
& Y is compact & f is_continuous_on Y ex x1,x2 st x1 in Y & x2 in Y & f/.x1 =
upper_bound (f.:Y) & f/.x2 = lower_bound (f.:Y)
proof
let f be PartFunc of the carrier of S,REAL;
let Y such that
A1: Y <> {} and
A2: Y c= dom f and
A3: Y is compact and
A4: f is_continuous_on Y;
A5: dom (f|Y) = dom f /\ Y by RELAT_1:61
.= Y by A2,XBOOLE_1:28;
f|Y is_continuous_on Y
proof
thus Y c= dom (f|Y) by A5;
let r be Point of S;
assume r in Y;
then f|Y is_continuous_in r by A4;
hence thesis by RELAT_1:72;
end;
then consider x1,x2 such that
A6: x1 in dom (f|Y) & x2 in dom (f|Y) and
A7: (f|Y)/.x1 = upper_bound (rng (f|Y)) & (f|Y)/.x2 = lower_bound (rng
(f|Y)) by A1,A3,A5,Th33;
take x1,x2;
thus x1 in Y & x2 in Y by A5,A6;
(f|Y)/.x1 =f/.x1 & (f|Y)/.x2 =f/.x2 by A6,PARTFUN2:15;
hence thesis by A7,RELAT_1:115;
end;
definition
let S,T;
let X,f;
pred f is_Lipschitzian_on X means
X c= dom f & ex r st 0<r & for x1,
x2 st x1 in X & x2 in X holds ||.f/.x1-f/.x2.||<=r*||.x1-x2.||;
end;
definition
let S;
let X;
let f be PartFunc of the carrier of S,REAL;
pred f is_Lipschitzian_on X means
X c= dom f & ex r st 0<r & for x1,
x2 st x1 in X & x2 in X holds |.f/.x1-f/.x2.|<=r*||.x1-x2.||;
end;
theorem Th38:
f is_Lipschitzian_on X & X1 c= X implies f is_Lipschitzian_on X1
proof
assume that
A1: f is_Lipschitzian_on X and
A2: X1 c= X;
X c= dom f by A1;
hence X1 c= dom f by A2;
consider s such that
A3: 0<s and
A4: for x1,x2 st x1 in X & x2 in X holds ||. f/.x1-f/.x2.||<=s*||. x1-x2
.|| by A1;
take s;
thus 0<s by A3;
let x1,x2;
assume x1 in X1 & x2 in X1;
hence thesis by A2,A4;
end;
theorem
f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 implies f1+f2
is_Lipschitzian_on X /\ X1
proof
assume that
A1: f1 is_Lipschitzian_on X and
A2: f2 is_Lipschitzian_on X1;
A3: f1 is_Lipschitzian_on X /\ X1 by A1,Th38,XBOOLE_1:17;
then consider s such that
A4: 0<s and
A5: for x1,x2 st x1 in X /\ X1 & x2 in X /\ X1 holds ||. f1/.x1-f1/.x2
.||<=s*||. x1-x2 .||;
A6: f2 is_Lipschitzian_on X /\ X1 by A2,Th38,XBOOLE_1:17;
then
A7: X /\ X1 c= dom f2;
X /\ X1 c= dom f1 by A3;
then X /\ X1 c= dom f1 /\ dom f2 by A7,XBOOLE_1:19;
hence
A8: X /\ X1 c= dom (f1+f2) by VFUNCT_1:def 1;
consider g such that
A9: 0<g and
A10: for x1,x2 st x1 in X /\ X1 & x2 in X /\ X1 holds ||. f2/.x1-f2/.x2
.||<=g*||. x1-x2 .|| by A6;
take p=s+g;
0+0<s+g by A4,A9;
hence 0<p;
let x1,x2;
assume that
A11: x1 in X/\X1 and
A12: x2 in X/\X1;
A13: ||. f2/.x1-f2/.x2.||<=g*||. x1-x2.|| by A10,A11,A12;
||. f1/.x1-f1/.x2.||<=s*||. x1-x2.|| by A5,A11,A12;
then
A14: ||. f1/.x1-f1/.x2.||+||. f2/.x1-f2/.x2.||<= s*||. x1-x2.||+g*||. x1-x2
.|| by A13,XREAL_1:7;
||. (f1+f2)/.x1-(f1+f2)/.x2 .|| = ||. f1/.x1 + f2/.x1-(f1+f2)/.x2.|| by A8
,A11,VFUNCT_1:def 1
.= ||. f1/.x1 + f2/.x1 - (f1/.x2+f2/.x2) .|| by A8,A12,VFUNCT_1:def 1
.= ||. f1/.x1 + (f2/.x1 - (f1/.x2+f2/.x2)).|| by RLVECT_1:def 3
.= ||. 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:def 3
.= ||. f1/.x1 - f1/.x2 + (f2/.x1-f2/.x2).|| by RLVECT_1:def 3;
then
||. (f1+f2)/.x1-(f1+f2)/.x2.|| <=||. f1/.x1-f1/.x2.||+||. f2/.x1-f2/.x2
.|| by NORMSP_1:def 1;
hence thesis by A14,XXREAL_0:2;
end;
theorem
f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 implies f1-f2
is_Lipschitzian_on X /\ X1
proof
assume that
A1: f1 is_Lipschitzian_on X and
A2: f2 is_Lipschitzian_on X1;
A3: f1 is_Lipschitzian_on X /\ X1 by A1,Th38,XBOOLE_1:17;
then consider s such that
A4: 0<s and
A5: for x1,x2 st x1 in X /\ X1 & x2 in X /\ X1 holds ||. f1/.x1-f1/.x2
.||<=s*||. x1-x2.||;
A6: f2 is_Lipschitzian_on X /\ X1 by A2,Th38,XBOOLE_1:17;
then
A7: X /\ X1 c= dom f2;
X /\ X1 c= dom f1 by A3;
then X /\ X1 c= dom f1 /\ dom f2 by A7,XBOOLE_1:19;
hence
A8: X /\ X1 c= dom (f1-f2) by VFUNCT_1:def 2;
consider g such that
A9: 0<g and
A10: for x1,x2 st x1 in X /\ X1 & x2 in X /\ X1 holds ||. f2/.x1-f2/.x2
.||<=g*||. x1-x2.|| by A6;
take p=s+g;
0+0<s+g by A4,A9;
hence 0<p;
let x1,x2;
assume that
A11: x1 in X/\X1 and
A12: x2 in X/\X1;
A13: ||. f2/.x1-f2/.x2.||<=g*||. x1-x2.|| by A10,A11,A12;
||. f1/.x1-f1/.x2.||<=s*||. x1-x2.|| by A5,A11,A12;
then
A14: ||. f1/.x1-f1/.x2.||+||. f2/.x1-f2/.x2.||<= s*||. x1-x2.||+g*||. x1-x2
.|| by A13,XREAL_1:7;
||. (f1-f2)/.x1-(f1-f2)/.x2.|| = ||. f1/.x1 - f2/.x1-(f1-f2)/.x2.|| by A8,A11
,VFUNCT_1:def 2
.= ||. f1/.x1 - f2/.x1 - (f1/.x2-f2/.x2).|| by A8,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:def 3
.= ||. f1/.x1 - (f1/.x2 + (f2/.x1-f2/.x2)).|| by RLVECT_1:def 3
.= ||. f1/.x1 - f1/.x2 - (f2/.x1-f2/.x2).|| by RLVECT_1:27;
then ||. (f1-f2)/.x1-(f1-f2)/.x2.|| <=||. f1/.x1-f1/.x2.||+||. f2/.x1-f2 /.
x2.|| by NORMSP_1:3;
hence thesis by A14,XXREAL_0:2;
end;
theorem Th41:
f is_Lipschitzian_on X implies p(#)f is_Lipschitzian_on X
proof
assume
A1: f is_Lipschitzian_on X;
then consider s such that
A2: 0<s and
A3: for x1,x2 st x1 in X & x2 in X holds ||. f/.x1-f/.x2.||<=s*||. x1-x2
.||;
X c= dom f by A1;
hence
A4: X c= dom (p(#)f) by VFUNCT_1:def 4;
per cases;
suppose
A5: p=0;
take s;
thus 0<s by A2;
let x1,x2;
assume that
A6: x1 in X and
A7: x2 in X;
0<=||. x1-x2.|| by NORMSP_1:4;
then
A8: s*0<=s*||. x1-x2.|| by A2;
||. (p(#)f)/.x1-(p(#)f)/.x2.|| = ||. p*(f/.x1)-(p(#)f)/.x2.||
by A4,A6,VFUNCT_1: def 4
.= ||. 0.T-(p(#)f)/.x2.|| by A5,RLVECT_1:10
.= ||. 0.T - p*(f/.x2).|| by A4,A7,VFUNCT_1:def 4
.= ||. 0.T-0.T.|| by A5,RLVECT_1:10
.= ||. 0.T.||
.= 0 by NORMSP_1:1;
hence ||. (p(#)f)/.x1-(p(#)f)/.x2.|| <=s*||. x1-x2.|| by A8;
end;
suppose
A9: p<>0;
take g = |.p.| *s;
0<|.p.| by A9,COMPLEX1:47;
then 0*s<|.p.|*s by A2,XREAL_1:68;
hence 0<g;
let x1,x2;
assume that
A10: x1 in X and
A11: x2 in X;
0<=|.p.| by COMPLEX1:46;
then
A12: |.p.|*||. f/.x1-f/.x2.|| <=|.p.|*(s*||. x1-x2.||)
by A3,A10,A11,XREAL_1:64;
||. (p(#)f)/.x1-(p(#)f)/.x2.|| = ||. p*(f/.x1)-(p(#)f)/.x2.||
by A4,A10,VFUNCT_1: def 4
.= ||. p*(f/.x1) - p*(f/.x2).|| by A4,A11,VFUNCT_1:def 4
.= ||. p*(f/.x1 - f/.x2).|| by RLVECT_1:34
.= |.p.|*||. f/.x1 - f/.x2.|| by NORMSP_1:def 1;
hence ||. (p(#)f)/.x1-(p(#)f)/.x2.|| <= g*||. x1-x2.|| by A12;
end;
end;
theorem
f is_Lipschitzian_on X implies -f is_Lipschitzian_on X & ||.f.||
is_Lipschitzian_on X
proof
assume
A1: f is_Lipschitzian_on X;
then consider s such that
A2: 0<s and
A3: for x1,x2 st x1 in X & x2 in X holds ||. f/.x1-f/.x2.||<=s*||. x1-x2
.||;
-f=(-1)(#)f by VFUNCT_1:23;
hence -f is_Lipschitzian_on X by A1,Th41;
X c= dom f by A1;
hence
A4: X c= dom (||.f.|| ) by NORMSP_0:def 3;
take s;
thus 0<s by A2;
let x1,x2;
assume that
A5: x1 in X and
A6: x2 in X;
|. (||.f.|| )/.x1-(||.f.|| )/.x2 .| =|. (||.f.|| ).x1-(||.f.|| )/.x2
.| by A4,A5,PARTFUN1:def 6
.=|. (||.f.|| ).x1-(||.f.|| ).x2 .| by A4,A6,PARTFUN1:def 6
.= |. ||. f/.x1.||-(||.f.|| ).x2 .| by A4,A5,NORMSP_0:def 3
.= |.||. f/.x1.|| - ||. f/.x2 .||.| by A4,A6,NORMSP_0:def 3;
then
A7: |. (||.f.|| )/.x1-(||.f.|| )/.x2 .| <= ||. f/.x1-f/.x2.|| by NORMSP_1:9;
||. f/.x1-f/.x2 .||<=s*||. x1-x2.|| by A3,A5,A6;
hence thesis by A7,XXREAL_0:2;
end;
theorem Th43:
X c= dom f & f|X is constant implies f is_Lipschitzian_on X
proof
assume that
A1: X c= dom f and
A2: f|X is constant;
now
let x1,x2;
assume that
A3: x1 in X and
A4: x2 in X;
A5: x1 in X /\ dom f & x2 in X /\ dom f by A1,A3,A4,XBOOLE_0:def 4;
f/.x1= f.x1 by A1,A3,PARTFUN1:def 6
.= f.x2 by A2,A5,PARTFUN2:58
.= f/.x2 by A1,A4,PARTFUN1:def 6;
then ||. f/.x1-f/.x2.|| = ||. 0.T .|| by RLVECT_1:15
.= 0 by NORMSP_1:1;
hence ||. f/.x1-f/.x2.|| <= 1*||. x1-x2 .|| by NORMSP_1:4;
end;
hence thesis by A1;
end;
theorem
id Y is_Lipschitzian_on Y
proof
reconsider r=1 as Real;
thus Y c= dom(id Y) by RELAT_1:45;
take r;
thus r>0;
let x1,x2;
assume that
A1: x1 in Y and
A2: x2 in Y;
||. (id Y)/.x1-(id Y)/.x2 .|| = ||. x1-(id Y)/.x2 .|| by A1,PARTFUN2:6
.= r*||. x1-x2 .|| by A2,PARTFUN2:6;
hence thesis;
end;
theorem Th45:
f is_Lipschitzian_on X implies f is_continuous_on X
proof
assume
A1: f is_Lipschitzian_on X;
then consider r such that
A2: 0<r and
A3: for x1,x2 st x1 in X & x2 in X holds ||. f/.x1-f/.x2.||<=r*||. x1-x2
.||;
A4: X c= dom f by A1;
then
A5: dom (f|X) = X by RELAT_1:62;
now
let x0 such that
A6: x0 in X;
now
let g such that
A7: 0<g;
reconsider s=g/r as Real;
take s9=s;
A8: now
let x1;
assume that
A9: x1 in dom (f|X) and
A10: ||. x1- x0 .|| <s;
r*||. x1- x0 .|| <(g/r)*r by A2,A10,XREAL_1:68;
then
A11: r*||. x1- x0 .|| <g by A2,XCMPLX_1:87;
||. f/.x1- f/.x0 .|| <=r*||. x1- x0 .|| by A3,A5,A6,A9;
then ||. f/.x1- f/.x0 .|| <g by A11,XXREAL_0:2;
then ||. (f|X)/.x1-f/.x0 .||<g by A9,PARTFUN2:15;
hence ||. (f|X)/.x1-(f|X)/.x0 .||<g by A5,A6,PARTFUN2:15;
end;
0<r" & s9=g*r" by A2,XCMPLX_0:def 9;
hence
0<s9 & for x1 st x1 in dom (f|X) & ||. x1- x0 .|| <s9 holds ||. (f|
X)/.x1-(f|X)/.x0.||<g by A7,A8,XREAL_1:129;
end;
hence f|X is_continuous_in x0 by A5,A6,Th7;
end;
hence thesis by A4;
end;
theorem Th46:
for f be PartFunc of the carrier of S, REAL st f
is_Lipschitzian_on X holds f is_continuous_on X
proof
let f be PartFunc of the carrier of S, REAL;
assume
A1: f is_Lipschitzian_on X;
then consider r such that
A2: 0<r and
A3: for x1,x2 st x1 in X & x2 in X holds |.f/.x1-f/.x2.|<=r*||. x1-x2
.||;
A4: X c= dom f by A1;
then
A5: dom (f|X) = X by RELAT_1:62;
now
let x0 such that
A6: x0 in X;
now
let g such that
A7: 0<g;
reconsider s=g/r as Real;
take s9=s;
A8: now
let x1;
assume that
A9: x1 in dom (f|X) and
A10: ||. x1- x0 .|| <s;
r*||. x1- x0 .|| <(g/r)*r by A2,A10,XREAL_1:68;
then
A11: r*||. x1- x0 .|| <g by A2,XCMPLX_1:87;
|. f/.x1- f/.x0 .| <=r*||. x1- x0 .|| by A3,A5,A6,A9;
then |. f/.x1- f/.x0 .| <g by A11,XXREAL_0:2;
then |. (f|X)/.x1-f/.x0 .|<g by A9,PARTFUN2:15;
hence |. (f|X)/.x1-(f|X)/.x0 .|<g by A5,A6,PARTFUN2:15;
end;
0<r" & s9=g*r" by A2,XCMPLX_0:def 9;
hence
0<s9 & for x1 st x1 in dom (f|X) & ||. x1- x0 .|| <s9 holds |. (f
|X)/.x1-(f|X)/.x0.|<g by A7,A8,XREAL_1:129;
end;
hence f|X is_continuous_in x0 by A5,A6,Th8;
end;
hence thesis by A4;
end;
theorem
for f st (ex r be Point of T st rng f = {r}) holds f is_continuous_on (dom f)
proof
let f;
given r be Point of T such that
A1: rng f = {r};
now
let x1,x2;
assume that
A2: x1 in dom f and
A3: x2 in dom f;
f.x2 in rng f by A3,FUNCT_1:def 3;
then f/.x2 in rng f by A3,PARTFUN1:def 6;
then
A4: 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.T .|| by A4,RLVECT_1:15
.= 0 by NORMSP_1:1;
hence ||. f/.x1-f/.x2.|| <= 1*||. x1-x2.|| by NORMSP_1:4;
end;
then f is_Lipschitzian_on dom f;
hence thesis by Th45;
end;
theorem
X c= dom f & f|X is constant implies f is_continuous_on X by Th43,Th45;
theorem Th49:
for f be PartFunc of S,S st (for x0 st x0 in dom f holds f/.x0 =
x0) holds f is_continuous_on dom f
proof
let f be PartFunc of S,S such that
A1: for x0 st x0 in dom f holds f/.x0 = x0;
now
let x1,x2;
assume that
A2: x1 in dom f and
A3: x2 in dom f;
f/.x1 = x1 by A1,A2;
hence ||. f/.x1-f/.x2.|| <= 1*||. x1-x2.|| by A1,A3;
end;
then f is_Lipschitzian_on dom f;
hence thesis by Th45;
end;
theorem
for f be PartFunc of S,S st f = id dom f holds f is_continuous_on dom f
proof
let f be PartFunc of S,S;
assume
A1: f = id dom f;
now
let x0 such that
A2: x0 in dom f;
thus f/.x0=f.x0 by A2,PARTFUN1:def 6
.= x0 by A1,A2,FUNCT_1:17;
end;
hence thesis by Th49;
end;
theorem
for f be PartFunc of S,S st Y c= dom f & f|Y = id Y holds f
is_continuous_on Y
proof
let f be PartFunc of S,S;
assume that
A1: Y c= dom f and
A2: f|Y = id Y;
now
let x1,x2;
assume that
A3: x1 in Y and
A4: x2 in Y;
x1 in dom f /\ Y by A1,A3,XBOOLE_0:def 4;
then
A5: x1 in dom (f|Y) by RELAT_1:61;
(f|Y).x1 = x1 by A2,A3,FUNCT_1:17;
then f.x1 = x1 by A5,FUNCT_1:47;
then
A6: f/.x1 = x1 by A1,A3,PARTFUN1:def 6;
x2 in dom f /\ Y by A1,A4,XBOOLE_0:def 4;
then
A7: x2 in dom (f|Y) by RELAT_1:61;
(f|Y).x2 = x2 by A2,A4,FUNCT_1:17;
then f.x2 = x2 by A7,FUNCT_1:47;
hence ||. f/.x1-f/.x2.|| <= 1*||. x1-x2.|| by A1,A4,A6,PARTFUN1:def 6;
end;
then f is_Lipschitzian_on Y by A1;
hence thesis by Th45;
end;
theorem
for f be PartFunc of S,S for r be Real for p be Point of S holds (X c=
dom f & (for x0 st x0 in X holds f/.x0 = r*x0+p) implies f is_continuous_on X )
proof
let f be PartFunc of S,S;
let r be Real;
let p be Point of S;
assume that
A1: X c= dom f and
A2: for x0 st x0 in X holds f/.x0 = r*x0+p;
now
0+0<|.r.|+1 by COMPLEX1:46,XREAL_1:8;
hence 0<|.r.|+1;
let x1,x2 be Point of S;
assume x1 in X & x2 in X;
then f/.x1 = r*x1+p & f/.x2 = r*x2+p by A2;
then
A3: ||. f/.x1-f/.x2.|| = ||. r*x1+(p-(p+r*x2)).|| by RLVECT_1:def 3
.= ||. r*x1+(p-p-r*x2).|| by RLVECT_1:27
.= ||. r*x1+(0.S-r*x2).|| by RLVECT_1:15
.= ||. r*x1-r*x2.||
.= ||. r*(x1-x2).|| by RLVECT_1:34
.= |.r.|*||. x1-x2.|| by NORMSP_1:def 1;
0<=||. x1-x2.|| by NORMSP_1:4;
then
||. f/.x1-f/.x2.|| + 0 <= |.r.|*||. x1-x2.|| + 1*||. x1-x2.|| by A3,
XREAL_1:7;
hence ||. f/.x1-f/.x2.|| <= (|.r.|+1)*||. x1-x2.||;
end;
then f is_Lipschitzian_on X by A1;
hence thesis by Th45;
end;
theorem Th53:
for f be PartFunc of the carrier of S,REAL st (for x0 st x0 in
dom f holds f/.x0 = ||. x0.|| ) holds f is_continuous_on (dom f)
proof
let f be PartFunc of the carrier of S,REAL;
assume
A1: for x0 st x0 in dom f holds f/.x0 = ||. x0 .||;
now
let x1,x2;
assume x1 in dom f & x2 in dom f;
then f/.x1 = ||. x1 .|| & f/.x2 = ||. x2.|| by A1;
hence |.f/.x1-f/.x2.| <= 1*||. x1-x2.|| by NORMSP_1:9;
end;
then f is_Lipschitzian_on dom f;
hence thesis by Th46;
end;
theorem
for f be PartFunc of the carrier of S,REAL st X c= dom f & (for x0 st
x0 in X holds f/.x0 = ||. x0.||) holds f is_continuous_on X
proof
let f be PartFunc of the carrier of S,REAL;
assume that
A1: X c= dom f and
A2: for x0 st x0 in X holds f/.x0 = ||. x0 .||;
X=dom f /\ X by A1,XBOOLE_1:28;
then
A3: X=dom(f|X) by RELAT_1:61;
now
let x0;
assume
A4: x0 in dom(f|X);
hence (f|X)/.x0=f/.x0 by PARTFUN2:15
.=||. x0 .|| by A2,A3,A4;
end;
then f|X is_continuous_on X by A3,Th53;
hence thesis by Th22;
end;