:: More on the Continuity of Real Functions
:: by Keiko Narita , Artur Kornilowicz and Yasunari Shidama
::
:: Received February 22, 2011
:: Copyright (c) 2011 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, XREAL_0, ORDINAL1, 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, VALUED_1, ZFMISC_1,
XXREAL_2, FCONT_1, NORMSP_1, STRUCT_0, PRE_TOPC, FINSEQ_1, CARD_3,
FINSET_1, MEMBERED, BORSUK_1, REAL_NS1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
RELSET_1, PARTFUN1, FUNCT_2, FINSET_1, NUMBERS, XXREAL_0, XREAL_0,
VALUED_0, VALUED_1, REAL_1, NAT_1, MEMBERED, COMPLEX1, BINOP_2, XXREAL_2,
FINSEQ_1, SEQ_1, SEQ_2, RCOMP_1, FCONT_1, STRUCT_0, PRE_TOPC, RLVECT_1,
NORMSP_0, NORMSP_1, EUCLID, NFCONT_1, REAL_NS1, PDIFF_1, INTEGR15,
VALUED_2, NFCONT_3, VFUNCT_1;
constructors REAL_1, COMPLEX1, SEQ_2, SEQ_4, SEQ_1, RELSET_1, FCONT_1,
NFCONT_1, VFUNCT_1, BINOP_2, PDIFF_1, INTEGR15, NFCONT_3, VALUED_2;
registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1,
MEMBERED, VALUED_0, FUNCT_2, XXREAL_2, FUNCT_1, ZFMISC_1, STRUCT_0,
EUCLID, FINSEQ_1, REAL_NS1, NFCONT_3, VALUED_2;
requirements REAL, NUMERALS, SUBSET, BOOLE;
definitions VALUED_1, FCONT_1, NFCONT_3, INTEGR15, TARSKI;
theorems TARSKI, NAT_1, FUNCT_1, FUNCT_2, PARTFUN1, XREAL_0, PARTFUN2,
RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_1, XXREAL_0,
ORDINAL1, XXREAL_2, VALUED_0, FCONT_1, NFCONT_1, NORMSP_0, FINSEQ_1,
FINSET_1, VFUNCT_1, REAL_NS1, SUBSET_1, PDIFF_8, NFCONT_3, VALUED_2;
schemes FUNCT_1, FINSEQ_1, PARTFUN2;
begin :: Basic Properties of the continuous functions of PartFunc of REAL,REAL n
reserve n,m,i,k for Element of NAT;
reserve x,X,X1 for set;
reserve r,p for Real;
reserve s,x0,x1,x2 for real number;
reserve f,f1,f2 for PartFunc of REAL,REAL n;
reserve h for PartFunc of REAL, the carrier of REAL-NS n;
definition let n,f,x0;
pred f is_continuous_in x0 means :Def1:
ex g be PartFunc of REAL,the carrier of REAL-NS n st
f=g & g is_continuous_in x0;
end;
theorem Def1Th:
h = f implies (f is_continuous_in x0 iff h is_continuous_in x0)
proof
assume AS: h = f;
hereby assume f is_continuous_in x0;
then ex g be PartFunc of REAL,the carrier of REAL-NS n st
f=g & g is_continuous_in x0 by Def1;
hence h is_continuous_in x0 by AS;
end;
thus thesis by AS,Def1;
end;
theorem Th1:
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;
consider g be PartFunc of REAL,the carrier of REAL-NS n such that
A3: f=g & g is_continuous_in x0 by A2,Def1;
g|X is_continuous_in x0 by A1,A3,NFCONT_3:6;
hence thesis by A3,Def1;
end;
theorem Th3:
f is_continuous_in x0 iff x0 in dom f &
for r st 0 PartFunc of Z,REAL means :Def4:
dom it = dom f & for x be set st x in dom it holds it/.x = |. f/.x .|;
existence
proof
consider g being Function such that
P3: dom g = dom f & for x be set st x in dom f holds g.x = F(x)
from FUNCT_1:sch 3;
now let y be set;
assume y in rng g;
then consider x be set such that
P41: x in dom g & y=g.x by FUNCT_1:def 5;
g.x = F(x) by P3,P41;
hence y in REAL by P41;
end;
then rng g c= REAL by TARSKI:def 3;
then g in PFuncs(Z,REAL) by P3,PARTFUN1:def 5;
then reconsider g as PartFunc of Z,REAL by PARTFUN1:120;
take g;
thus dom g = dom f by P3;
let x be set;
assume P6: x in dom g;
then g.x = F(x) by P3;
hence thesis by PARTFUN1:def 8,P6;
end;
uniqueness
proof
let g1,g2 be PartFunc of Z,REAL such that
A1:dom g1 = dom f & for x be set st x in dom g1 holds g1/.x = F(x) and
A2:dom g2 = dom f & for x be set st x in dom g2 holds g2/.x = F(x);
now let x be Element of Z;
assume P10:x in dom g1; then
P12: g1/.x = |. f/.x .| by A1;
g1/.x= g2/.x by A2,P12,A1,P10;
then g1.x= g2/.x by P10,PARTFUN1:def 8;
hence g1.x= g2.x by A1,A2,P10,PARTFUN1:def 8;
end;
hence g1=g2 by PARTFUN1:34,A1,A2;
end;
end;
definition
let n be Element of NAT;
let Z be non empty set;
let f be PartFunc of Z,REAL n;
deffunc G(set) = - f/.$1;
defpred P[set] means $1 in dom f;
func -f -> PartFunc of Z, REAL n means :Def5:
dom it = dom f & for c be set st c in dom it holds it/.c = - (f/.c);
existence
proof
consider F being PartFunc of Z,REAL n such that
A3: for c be Element of Z holds c in dom F iff P[c] and
A4: for c be Element of Z st c in dom F holds F/.c = G(c) from PARTFUN2:sch 2;
take F;
thus thesis by A3,A4,SUBSET_1:8;
end;
uniqueness
proof
let g1,g2 be PartFunc of Z,REAL n such that
A1: dom g1 = dom f & for x be set st x in dom g1 holds g1/.x = -f/.x and
A2: dom g2 = dom f & for x be set st x in dom g2 holds g2/.x = -f/.x;
now let x be Element of Z;
assume P10:x in dom g1; then
P12: g1/.x = - f/.x by A1;
g1/.x= g2/.x by A2,P12,A1,P10;
then g1.x= g2/.x by P10,PARTFUN1:def 8;
hence g1.x= g2.x by A1,A2,P10,PARTFUN1:def 8;
end;
hence g1=g2 by PARTFUN1:34,A1,A2;
end;
end;
theorem LM003A:
for f1,f2 be PartFunc of REAL,the carrier of REAL-NS n,
g1,g2 be PartFunc of REAL,REAL n st f1=g1 & f2=g2 holds
f1+f2 = g1+g2
proof
let f1,f2 be PartFunc of REAL,the carrier of REAL-NS n,
g1,g2 be PartFunc of REAL,REAL n;
assume AS: f1=g1 & f2=g2;
C1: dom(f1+f2) = dom f1 /\ dom f2 by VFUNCT_1:def 1; then
A2: dom(f1+f2) = dom(g1+g2) by AS,VALUED_2:def 45;
B1: now
let x be Element of REAL;
assume A3: x in dom(f1+f2); then
V: x in dom g1 & x in dom g2 by C1,AS,XBOOLE_0:def 4;
W: f1/.x=g1/.x & f2/.x=g2/.x by AS,REAL_NS1:def 4;
g1/.x = g1.x & g2/.x = g2.x by V,PARTFUN1:def 8; then
R: f1/.x + f2/.x = g1.x + g2.x by REAL_NS1:2,W;
(f1+f2)/.x = f1/.x + f2/.x by A3,VFUNCT_1:def 1; then
(f1+f2).x = f1/.x + f2/.x by PARTFUN1:def 8,A3;
hence (f1+f2).x = (g1+g2).x by R,A2,A3,VALUED_2:def 45;
end;
f1+f2 is PartFunc of REAL,REAL n by REAL_NS1:def 4;
hence thesis by A2,B1,PARTFUN1:34;
end;
theorem LM003B:
for f1 be PartFunc of REAL,the carrier of REAL-NS n,
g1 be PartFunc of REAL,REAL n,
a be Real st f1=g1 holds
a(#)f1 = a(#)g1
proof
let f1 be PartFunc of REAL,the carrier of REAL-NS n,
g1 be PartFunc of REAL,REAL n,
a be Real;
assume AS: f1=g1;
S: dom(a(#)f1) = dom f1 by VFUNCT_1:def 4; then
A2: dom(a(#)f1) = dom(a(#)g1) by AS,VALUED_2:def 39;
B1: now
let x be Element of REAL;
assume A3: x in dom(a(#)f1); then
B: g1.x = g1/.x by PARTFUN1:def 8,AS,S;
f1/.x=g1/.x by AS,REAL_NS1:def 4; then
A5: a*(f1/.x)=a*(g1/.x) by REAL_NS1:3;
A6: (a(#)f1)/.x = a*(f1/.x) by A3,VFUNCT_1:def 4;
(a(#)g1).x = a(#)(g1.x) by A2,A3,VALUED_2:def 39;
hence (a(#)f1).x = (a(#)g1).x by A3,A5,A6,PARTFUN1:def 8,B;
end;
a(#)f1 is PartFunc of REAL,REAL n by REAL_NS1:def 4;
hence thesis by A2,B1,PARTFUN1:34;
end;
theorem
for f1 be PartFunc of REAL, REAL n holds (-1)(#)f1 = -f1
proof
let f1 be PartFunc of REAL, REAL n;
F: dom((-1)(#)f1) = dom f1 by VALUED_2:def 39; then
A1: dom((-1)(#)f1) = dom(-f1) by Def5;
now let x be Element of REAL;
assume A2: x in dom((-1)(#)f1);
G: f1.x = f1/.x by F,PARTFUN1:def 8,A2;
A5: (-f1)/.x = -(f1/.x) by A1,A2,Def5;
(f1[#](-1)).x = (-1)(#)(f1.x) by A2,VALUED_2:def 39;
hence ((-1)(#)f1).x = (-f1).x by PARTFUN1:def 8,G,A1,A2,A5;
end;
hence thesis by A1,PARTFUN1:34;
end;
theorem LM003E:
for f1 be PartFunc of REAL,the carrier of REAL-NS n,
g1 be PartFunc of REAL,REAL n st f1=g1 holds
-f1 = -g1
proof
let f1 be PartFunc of REAL,the carrier of REAL-NS n,
g1 be PartFunc of REAL,REAL n;
assume AS: f1=g1;
dom(-f1) = dom f1 by VFUNCT_1:def 6; then
A2: dom(-f1) = dom(-g1) by AS,Def5;
B1: now
let x be Element of REAL;
assume A3: x in dom(-f1);
f1/.x=g1/.x by AS,REAL_NS1:def 4; then
A5: -(f1/.x)=-(g1/.x) by REAL_NS1:4;
A6: (-f1)/.x = -(f1/.x) by A3,VFUNCT_1:def 6;
(-g1)/.x = -(g1/.x) by A2,A3,Def5;
then (-f1).x = (-g1)/.x by A3,A5,A6,PARTFUN1:def 8;
hence (-f1).x = (-g1).x by A2,A3,PARTFUN1:def 8;
end;
-f1 is PartFunc of REAL,REAL n by REAL_NS1:def 4;
hence -f1 = -g1 by A2,B1,PARTFUN1:34;
end;
theorem LM003F:
for f1 be PartFunc of REAL,the carrier of REAL-NS n,
g1 be PartFunc of REAL,REAL n st f1=g1 holds
||. f1 .|| = |. g1 .|
proof
let f1 be PartFunc of REAL,the carrier of REAL-NS n,
g1 be PartFunc of REAL,REAL n;
assume AS: f1=g1;
dom (||. f1 .||) = dom f1 by NORMSP_0:def 3; then
A2: dom (||. f1 .||) = dom(|. g1 .|) by AS,Def4;
now
let x be Element of REAL;
assume A3: x in dom ||. f1 .||;
A4: f1/.x=g1/.x by AS,REAL_NS1:def 4;
set y1=g1/.x;
A5: ||. f1/.x .||=|. y1 .| by A4,REAL_NS1:1;
A6: (||. f1 .||).x = ||. f1/.x .|| by A3,NORMSP_0:def 3;
|. g1 .| /.x = |. g1/.x .| by A2,A3,Def4;
hence (||. f1 .||).x = (|. g1 .|).x by A2,A3,A5,A6,PARTFUN1:def 8;
end;
hence thesis by A2,PARTFUN1:34;
end;
theorem LM003D:
for f1,f2 be PartFunc of REAL,the carrier of REAL-NS n,
g1,g2 be PartFunc of REAL,REAL n st f1=g1 & f2=g2 holds
f1-f2 = g1-g2
proof
let f1,f2 be PartFunc of REAL,the carrier of REAL-NS n,
g1,g2 be PartFunc of REAL,REAL n;
assume AS: f1=g1 & f2=g2;
K: dom(f1-f2) = dom f1 /\ dom f2 by VFUNCT_1:def 2; then
A2: dom(f1-f2) = dom(g1-g2) by AS,VALUED_2:def 46;
B1: now
let x be Element of REAL;
assume A3: x in dom(f1-f2);
a: f1/.x=g1/.x & f2/.x=g2/.x by AS,REAL_NS1:def 4;
x in dom f1 & x in dom f2 by A3,K,XBOOLE_0:def 4; then
g1.x = g1/.x & g2/.x = g2.x by AS,PARTFUN1:def 8; then
A5: f1/.x - f2/.x = g1.x - g2.x by REAL_NS1:5,a;
A6: (f1-f2)/.x = f1/.x - f2/.x by A3,VFUNCT_1:def 2;
(f1-f2)/.x = (f1-f2).x by A3,PARTFUN1:def 8;
hence (f1-f2).x = (g1-g2).x by A5,A6,A2,A3,VALUED_2:def 46;
end;
f1-f2 is PartFunc of REAL,REAL n by REAL_NS1:def 4;
hence f1-f2 = g1-g2 by A2,B1,PARTFUN1:34;
end;
theorem
f is_continuous_in x0 iff
x0 in dom f & for N1 be Subset of REAL n st ex r be Real st 0 < r &
{y where y is Element of REAL n: |.y-f/.x0.| < r} = N1
ex N being Neighbourhood of x0 st
for x1 st x1 in dom f & x1 in N holds f/.x1 in N1
proof
thus f is_continuous_in x0 implies x0 in dom f &
for N1 be Subset of REAL n st ex r be Real st 0 < r &
{y where y is Element of REAL n: |.y-f/.x0.| < r} = N1
ex N being Neighbourhood of x0
st for x1 st x1 in dom f & x1 in N holds f/.x1 in N1
proof
assume f is_continuous_in x0;
then consider g be PartFunc of REAL,the carrier of REAL-NS n such that
B2: f=g & g is_continuous_in x0 by Def1;
thus x0 in dom f by B2,NFCONT_3:9;
let N01 be Subset of REAL n such that
X2: ex r be Real st 0 < r &
{y where y is Element of REAL n: |.y-f/.x0.| < r} = N01;
consider r such that
A2: 0 continuous PartFunc of REAL,REAL n;
coherence
proof
let f be PartFunc of REAL,REAL n;
assume
A1: f is constant;
now
reconsider s = 1 as real number;
let x0,r;
assume that
A2: x0 in dom f and
A3: 0 continuous PartFunc of REAL,REAL n;
coherence
proof
for x0 st x0 in dom(f|X) holds f|X is_continuous_in x0
proof
let x0;
assume
A1: x0 in dom(f|X);
then x0 in dom f by RELAT_1:86; then
A2: f is_continuous_in x0 by Def2;
x0 in X by A1,RELAT_1:86;
hence thesis by A2,Th1;
end;
hence thesis by Def2;
end;
end;
theorem
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:103;
hence thesis by A1;
end;
registration let n;
cluster empty -> continuous PartFunc of REAL,REAL n;
coherence;
end;
registration let n,f;
let X be trivial set;
cluster f|X -> continuous PartFunc of REAL,REAL n;
coherence
proof
reconsider g= f as PartFunc of REAL,the carrier of REAL-NS n
by REAL_NS1:def 4;
g|X is continuous PartFunc of REAL,the carrier of REAL-NS n;
hence thesis by Def2Th;
end;
end;
registration let n;
let f1,f2 be continuous PartFunc of REAL,REAL n;
cluster f1+f2 -> continuous PartFunc of REAL,REAL n;
coherence
proof
reconsider g1= f1,g2=f2 as PartFunc of REAL,the carrier of REAL-NS n
by REAL_NS1:def 4;
P1: g1 is continuous & g2 is continuous by Def2Th;
g1+g2= f1+f2 by LM003A;
hence thesis by P1,Def2Th;
end;
end;
theorem
X c= dom f1 /\ dom f2 & f1|X is continuous & f2|X is continuous
implies (f1+f2) |X is continuous & (f1-f2) |X is continuous
proof
assume AS: X c= dom f1 /\ dom f2 & f1|X is continuous & f2|X
is continuous;
reconsider g1=f1,g2=f2 as PartFunc of REAL,the carrier of REAL-NS n
by REAL_NS1:def 4;
P2: g1|X is continuous by AS,Def2Th;
g2|X is continuous by AS,Def2Th; then
P3: (g1+g2) |X is continuous & (g1-g2) |X is continuous
by AS,P2,NFCONT_3:19;
P4: g1+g2 = f1+f2 by LM003A;
g1-g2 = f1-f2 by LM003D;
hence thesis by P3,P4,Def2Th;
end;
theorem
X c= dom f1 & X1 c= dom f2 & f1|X is continuous & f2|X1 is continuous
implies (f1+f2) | (X /\ X1) is continuous & (f1-f2) | (X /\ X1) is continuous
proof
assume AS: X c= dom f1 & X1 c= dom f2 & f1|X is continuous & f2|X1
is continuous;
reconsider g1=f1,g2=f2 as PartFunc of REAL,the carrier of REAL-NS n
by REAL_NS1:def 4;
P2: g1|X is continuous by AS,Def2Th;
g2|X1 is continuous by AS,Def2Th; then
P3: (g1+g2) | (X /\ X1) is continuous & (g1-g2) | (X /\ X1) is continuous
by AS,P2,NFCONT_3:20;
P4: g1+g2 = f1+f2 by LM003A;
g1-g2 = f1-f2 by LM003D;
hence thesis by P3,P4,Def2Th;
end;
registration let n;
let f be continuous PartFunc of REAL,REAL n;
let r;
cluster r(#)f -> continuous PartFunc of REAL,REAL n;
coherence
proof
reconsider g= f as PartFunc of REAL,the carrier of REAL-NS n
by REAL_NS1:def 4;
P1: g is continuous by Def2Th;
r(#)g = r(#)f by LM003B;
hence thesis by P1,Def2Th;
end;
end;
theorem
X c= dom f & f|X is continuous implies (r(#)f) | X is continuous
proof
assume AS:X c= dom f & f|X is continuous;
reconsider g= f as PartFunc of REAL,the carrier of REAL-NS n
by REAL_NS1:def 4;
g|X is continuous PartFunc of REAL,the carrier of REAL-NS n by AS,Def2Th;
then
P1: (r(#)g) | X is continuous by AS,NFCONT_3:21;
r(#)g = r(#)f by LM003B;
hence thesis by P1,Def2Th;
end;
theorem
X c= dom f & f|X is continuous
implies |. f .| |X is continuous & (-f) | X is continuous
proof
assume AS: X c= dom f & f|X is continuous;
reconsider g= f as PartFunc of REAL,the carrier of REAL-NS n
by REAL_NS1:def 4;
g|X is continuous by AS,Def2Th; then
P1: ||. g .|| |X is continuous & (-g) | X is continuous by AS,NFCONT_3:22;
hence |. f .| |X is continuous by LM003F;
-g = - f by LM003E;
hence (-f) | X is continuous by P1,Def2Th;
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 AS:
f is total & (for x1,x2 holds f/.(x1+x2) = f/.x1 + f/.x2);
given x0 such that
P3: f is_continuous_in x0;
reconsider g= f as PartFunc of REAL,the carrier of REAL-NS n
by REAL_NS1:def 4;
P2: now let x1,x2;
P21: g/.x1 = f/.x1 & g/.x2 = f/.x2 by REAL_NS1:def 4;
thus g/.(x1+x2) = f/.(x1+x2) by REAL_NS1:def 4
.=f/.x1 + f/.x2 by AS
.= g/.x1 + g/.x2 by P21,REAL_NS1:2;
end;
g is_continuous_in x0 by P3,Def1Th;
then g|REAL is continuous by AS,P2,NFCONT_3:23;
hence thesis by Def2Th;
end;
theorem
for Y be Subset of REAL-NS n st
dom f is compact & f| (dom f) is continuous & Y = rng f
holds Y is compact
proof
let Y be Subset of REAL-NS n;
assume AS:dom f is compact & f| (dom f) is continuous & Y = (rng f);
reconsider g= f as PartFunc of REAL,the carrier of REAL-NS n
by REAL_NS1:def 4;
g| (dom g) is continuous by AS,Def2Th;
hence Y is compact by AS,NFCONT_3:24;
end;
theorem
for Y be Subset of REAL, Z be Subset of REAL-NS n st
Y c= dom f & Z = f.:Y & Y is compact & f|Y is continuous
holds Z is compact
proof
let Y be Subset of REAL, Z be Subset of REAL-NS n;
assume
AS: Y c= dom f & Z = (f.:Y) & Y is compact & f|Y is continuous;
reconsider g = f as PartFunc of REAL,the carrier of REAL-NS n
by REAL_NS1:def 4;
g|Y is continuous by AS,Def2Th;
hence Z is compact by AS,NFCONT_3:25;
end;
definition let n,f;
attr f is Lipschitzian means :Def6:
ex g be PartFunc of REAL,the carrier of REAL-NS n st g=f &
g is Lipschitzian;
end;
theorem Def6Th:
f is Lipschitzian iff
ex r be real number st 0 Lipschitzian PartFunc of REAL,REAL n;
coherence
proof
let f be PartFunc of REAL,REAL n;
reconsider g = f as PartFunc of REAL,the carrier of REAL-NS n
by REAL_NS1:def 4;
assume f is empty;
then g is empty;
hence thesis by Def6Th1;
end;
end;
registration let n;
cluster empty PartFunc of REAL,REAL n;
existence
proof
reconsider e = {} as PartFunc of REAL,REAL n by RELSET_1:25;
take e;
thus thesis;
end;
end;
registration let n;
let f be Lipschitzian PartFunc of REAL,REAL n, X be set;
cluster f|X -> Lipschitzian PartFunc of REAL,REAL n;
coherence
proof
reconsider g= f as PartFunc of REAL,the carrier of REAL-NS n
by REAL_NS1:def 4;
g is Lipschitzian by Def6Th1;
then g|X is Lipschitzian;
hence thesis by Def6Th1;
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:103;
hence thesis by A1;
end;
registration let n;
let f1,f2 be Lipschitzian PartFunc of REAL,REAL n;
cluster f1+f2 -> Lipschitzian PartFunc of REAL,REAL n;
coherence
proof
reconsider g1=f1,g2=f2 as PartFunc of REAL,the carrier of REAL-NS n
by REAL_NS1:def 4;
P1:g1 is Lipschitzian & g2 is Lipschitzian by Def6Th1;
g1+g2 = f1+f2 by LM003A;
hence thesis by P1,Def6Th1;
end;
cluster f1-f2 -> Lipschitzian PartFunc of REAL,REAL n;
coherence
proof
reconsider g1=f1,g2=f2 as PartFunc of REAL,the carrier of REAL-NS n
by REAL_NS1:def 4;
P1:g1 is Lipschitzian & g2 is Lipschitzian by Def6Th1;
g1-g2 = f1-f2 by LM003D;
hence thesis by P1,Def6Th1;
end;
end;
theorem
f1|X is Lipschitzian & f2|X1 is Lipschitzian implies
(f1+f2) | (X /\ X1) is Lipschitzian
proof
assume
AS:f1|X is Lipschitzian & f2|X1 is Lipschitzian;
reconsider g1=f1,g2=f2 as PartFunc of REAL,the carrier of REAL-NS n
by REAL_NS1:def 4;
g1|X is Lipschitzian & g2|X1 is Lipschitzian by Def6Th1,AS; then
P1: (g1+g2) | (X /\ X1) is Lipschitzian by NFCONT_3:28;
g1+g2 = f1+f2 by LM003A;
hence thesis by P1,Def6Th1;
end;
theorem
f1|X is Lipschitzian & f2|X1 is Lipschitzian implies
(f1-f2) | (X /\ X1) is Lipschitzian
proof
assume
AS:f1|X is Lipschitzian & f2|X1 is Lipschitzian;
reconsider g1=f1,g2=f2 as PartFunc of REAL,the carrier of REAL-NS n
by REAL_NS1:def 4;
g1|X is Lipschitzian & g2|X1 is Lipschitzian by Def6Th1,AS;
then
P1: (g1-g2) | (X /\ X1) is Lipschitzian by NFCONT_3:29;
g1-g2 = f1-f2 by LM003D;
hence thesis by P1,Def6Th1;
end;
registration let n;
let f be Lipschitzian PartFunc of REAL, REAL n;
let p;
cluster p(#)f -> Lipschitzian PartFunc of REAL, REAL n;
coherence
proof
reconsider g= f as PartFunc of REAL,the carrier of REAL-NS n
by REAL_NS1:def 4;
P1: g is Lipschitzian by Def6Th1;
p(#)g = p(#)f by LM003B;
hence thesis by P1,Def6Th1;
end;
end;
theorem
f|X is Lipschitzian & X c= dom f implies (p(#)f) | X is Lipschitzian
proof
assume AS: f|X is Lipschitzian & X c= dom f;
reconsider g= f as PartFunc of REAL,the carrier of REAL-NS n
by REAL_NS1:def 4;
g|X is Lipschitzian by Def6Th1,AS; then
P1: (p(#)g) | X is Lipschitzian by NFCONT_3:30,AS;
p(#)g = p(#)f by LM003B;
hence thesis by P1,Def6Th1;
end;
registration let n;
let f be Lipschitzian PartFunc of REAL, REAL n;
cluster |. f .| -> Lipschitzian PartFunc of REAL,REAL;
coherence
proof
reconsider g= f as PartFunc of REAL,the carrier of REAL-NS n
by REAL_NS1:def 4;
g is Lipschitzian by Def6Th1;
then ||. g .|| is Lipschitzian;
hence thesis by LM003F;
end;
end;
theorem
f|X is Lipschitzian implies -(f|X) is Lipschitzian
& |. f .| |X is Lipschitzian & (-f) |X is Lipschitzian
proof
assume AS: f|X is Lipschitzian;
reconsider g= f as PartFunc of REAL,the carrier of REAL-NS n
by REAL_NS1:def 4;
g|X is Lipschitzian by AS,Def6Th1; then
P1: -(g|X) is Lipschitzian & (||. g .||) |X is Lipschitzian &
(-g) | X is Lipschitzian by NFCONT_3:31;
-(g|X) = -(f|X) by LM003E;
hence -(f|X) is Lipschitzian by P1,Def6Th1;
thus (|. f .|) |X is Lipschitzian by P1,LM003F;
-g = - f by LM003E;
hence thesis by P1,Def6Th1;
end;
registration let n;
cluster constant -> Lipschitzian PartFunc of REAL, REAL n;
coherence
proof
let f be PartFunc of REAL, REAL n;
assume
A1: f is constant;
reconsider g= f as PartFunc of REAL,the carrier of REAL-NS n
by REAL_NS1:def 4;
g is constant by A1;
hence thesis by Def6Th1;
end;
end;
registration let n;
cluster Lipschitzian -> continuous PartFunc of REAL, REAL n;
coherence
proof
let f be PartFunc of REAL, REAL n;
reconsider g= f as PartFunc of REAL,the carrier of REAL-NS n
by REAL_NS1:def 4;
assume f is Lipschitzian;
then g is Lipschitzian by Def6Th1;
hence thesis by Def2Th;
end;
end;
theorem
for r,p be Element of REAL n
st (for x0 st x0 in X holds f/.x0 = x0*r+p)
holds f|X is continuous
proof
let r,p be Element of REAL n;
assume AS: for x0 st x0 in X holds f/.x0 = x0*r+p;
reconsider g= f as PartFunc of REAL,the carrier of REAL-NS n
by REAL_NS1:def 4;
reconsider r0=r, p0=p as Point of REAL-NS n by REAL_NS1:def 4;
now let x0;
assume A1: x0 in X;
A2: x0*r = x0*r0 by REAL_NS1:3;
thus g/.x0 = f/.x0 by REAL_NS1:def 4
.= x0*r+p by A1,AS
.= x0*r0+p0 by A2,REAL_NS1:2;
end;
then g|X is continuous by NFCONT_3:33;
hence thesis by Def2Th;
end;
theorem X0:
for x0 be Element of REAL n st 1 <= i & i <= n
holds proj(i,n) is_continuous_in x0
proof
let x0 be Element of REAL n;
assume AS0: 1 <=i & i <= n;
P2:dom proj(i,n) = REAL n by FUNCT_2:def 1;
reconsider prg=proj(i,n) as PartFunc of the carrier of REAL-NS n,REAL
by REAL_NS1:def 4;
reconsider px0 = x0 as Element of the carrier of REAL-NS n
by REAL_NS1:def 4;
now let r be Real;
assume A3: 0