:: More on the Continuity of Real Functions
:: by Keiko Narita , Artur Kornilowicz and Yasunari Shidama
::
:: Received February 22, 2011
:: Copyright (c) 2011-2016 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, 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, XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
RELSET_1, PARTFUN1, FUNCT_2, FINSET_1, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, VALUED_1, REAL_1, MEMBERED, COMPLEX1, 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, RELSET_1, FCONT_1, NFCONT_1,
VFUNCT_1, BINOP_2, PDIFF_1, INTEGR15, NFCONT_3, VALUED_2, COMSEQ_2;
registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1,
VALUED_0, FUNCT_2, XXREAL_2, FUNCT_1, STRUCT_0, EUCLID, FINSEQ_1,
REAL_NS1, NFCONT_3, VALUED_2;
requirements REAL, NUMERALS, SUBSET, BOOLE;
definitions FCONT_1, NFCONT_3, TARSKI;
equalities VALUED_1, INTEGR15;
expansions FCONT_1, NFCONT_3, TARSKI;
theorems TARSKI, NAT_1, FUNCT_1, FUNCT_2, PARTFUN1, XREAL_0, PARTFUN2,
RELAT_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;
reserve f,f1,f2 for PartFunc of REAL,REAL n;
reserve h for PartFunc of REAL,REAL-NS n;
reserve W for non empty set;
definition let n,f,x0;
pred f is_continuous_in x0 means
ex g be PartFunc of REAL,REAL-NS n st f=g & g is_continuous_in x0;
end;
theorem
h = f implies (f is_continuous_in x0 iff h is_continuous_in x0);
theorem Th2:
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,REAL-NS n such that
A3: f=g & g is_continuous_in x0 by A2;
g|X is_continuous_in x0 by A1,A3,NFCONT_3:6;
hence thesis by A3;
end;
theorem Th3:
f is_continuous_in x0 iff x0 in dom f &
for r st 0 PartFunc of Z,REAL means :Def2:
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
A1: dom g = dom f & for x be object st x in dom f holds g.x = F(x)
from FUNCT_1:sch 3;
now let y be object;
assume y in rng g;
then consider x be object such that
A2: x in dom g & y=g.x by FUNCT_1:def 3;
g.x = F(x) by A1,A2;
hence y in REAL by A2,XREAL_0:def 1;
end;
then rng g c= REAL;
then g in PFuncs(Z,REAL) by A1,PARTFUN1:def 3;
then reconsider g as PartFunc of Z,REAL by PARTFUN1:46;
take g;
thus dom g = dom f by A1;
let x be set;
assume A3: x in dom g;
then g.x = F(x) by A1;
hence thesis by A3,PARTFUN1:def 6;
end;
uniqueness
proof
let g1,g2 be PartFunc of Z,REAL such that
A4:dom g1 = dom f & for x be set st x in dom g1 holds g1/.x = F(x) and
A5: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 A6:x in dom g1; then
A7: g1/.x = |. f/.x .| by A4;
g1/.x= g2/.x by A5,A7,A4,A6;
then g1.x= g2/.x by A6,PARTFUN1:def 6;
hence g1.x= g2.x by A4,A5,A6,PARTFUN1:def 6;
end;
hence g1=g2 by A4,A5,PARTFUN1:5;
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 :Def3:
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
A1: for c be Element of Z holds c in dom F iff P[c] and
A2: 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 A1,A2,SUBSET_1:3;
end;
uniqueness
proof
let g1,g2 be PartFunc of Z,REAL n such that
A3: dom g1 = dom f & for x be set st x in dom g1 holds g1/.x = -f/.x and
A4: 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 A5:x in dom g1; then
A6: g1/.x = - f/.x by A3;
g1/.x= g2/.x by A4,A6,A3,A5;
then g1.x= g2/.x by A5,PARTFUN1:def 6;
hence g1.x= g2.x by A3,A4,A5,PARTFUN1:def 6;
end;
hence g1=g2 by A3,A4,PARTFUN1:5;
end;
end;
theorem Th5:
for f1,f2 be PartFunc of W,REAL-NS n,
g1,g2 be PartFunc of W,REAL n st f1=g1 & f2=g2 holds
f1+f2 = g1+g2
proof
let f1,f2 be PartFunc of W,REAL-NS n,
g1,g2 be PartFunc of W,REAL n;
assume A1: f1=g1 & f2=g2;
A2: dom(f1+f2) = dom f1 /\ dom f2 by VFUNCT_1:def 1; then
A3: dom(f1+f2) = dom(g1+g2) by A1,VALUED_2:def 45;
A4: now
let x be Element of W;
assume A5: x in dom(f1+f2); then
A6: x in dom g1 & x in dom g2 by A2,A1,XBOOLE_0:def 4;
A7: f1/.x=g1/.x & f2/.x=g2/.x by A1,REAL_NS1:def 4;
g1/.x = g1.x & g2/.x = g2.x by A6,PARTFUN1:def 6; then
A8: f1/.x + f2/.x = g1.x + g2.x by A7,REAL_NS1:2;
(f1+f2)/.x = f1/.x + f2/.x by A5,VFUNCT_1:def 1; then
(f1+f2).x = f1/.x + f2/.x by A5,PARTFUN1:def 6;
hence (f1+f2).x = (g1+g2).x by A8,A3,A5,VALUED_2:def 45;
end;
f1+f2 is PartFunc of W,REAL n by REAL_NS1:def 4;
hence thesis by A3,A4,PARTFUN1:5;
end;
theorem Th6:
for f1 be PartFunc of W,REAL-NS n,
g1 be PartFunc of W,REAL n,
a be Real st f1=g1 holds
a(#)f1 = a(#)g1
proof
let f1 be PartFunc of W,REAL-NS n,
g1 be PartFunc of W,REAL n,
a be Real;
assume A1: f1=g1;
A2: dom(a(#)f1) = dom f1 by VFUNCT_1:def 4; then
A3: dom(a(#)f1) = dom(a(#)g1) by A1,VALUED_2:def 39;
A4: now
let x be Element of W;
assume A5: x in dom(a(#)f1); then
A6: g1.x = g1/.x by A1,A2,PARTFUN1:def 6;
f1/.x=g1/.x by A1,REAL_NS1:def 4; then
A7: a*(f1/.x)=a*(g1/.x) by REAL_NS1:3;
A8: (a(#)f1)/.x = a*(f1/.x) by A5,VFUNCT_1:def 4;
(a(#)g1).x = a(#)(g1.x) by A3,A5,VALUED_2:def 39;
hence (a(#)f1).x = (a(#)g1).x by A5,A7,A8,A6,PARTFUN1:def 6;
end;
a(#)f1 is PartFunc of W,REAL n by REAL_NS1:def 4;
hence thesis by A3,A4,PARTFUN1:5;
end;
theorem
for f1 be PartFunc of W,REAL n holds (-1)(#)f1 = -f1
proof
let f1 be PartFunc of W,REAL n;
A1: dom((-1)(#)f1) = dom f1 by VALUED_2:def 39; then
A2: dom((-1)(#)f1) = dom(-f1) by Def3;
now let x be Element of W;
assume A3: x in dom((-1)(#)f1);
A4: f1.x = f1/.x by A1,A3,PARTFUN1:def 6;
A5: (-f1)/.x = -(f1/.x) by A2,A3,Def3;
(f1[#](-1)).x = (-1)(#)(f1.x) by A3,VALUED_2:def 39;
hence ((-1)(#)f1).x = (-f1).x by A4,A2,A3,A5,PARTFUN1:def 6;
end;
hence thesis by A2,PARTFUN1:5;
end;
theorem Th8:
for f1 be PartFunc of W,REAL-NS n,
g1 be PartFunc of W,REAL n st f1=g1 holds
-f1 = -g1
proof
let f1 be PartFunc of W,REAL-NS n,
g1 be PartFunc of W,REAL n;
assume A1: f1=g1;
dom(-f1) = dom f1 by VFUNCT_1:def 5; then
A2: dom(-f1) = dom(-g1) by A1,Def3;
A3: now
let x be Element of W;
assume A4: x in dom(-f1);
f1/.x=g1/.x by A1,REAL_NS1:def 4; then
A5: -(f1/.x)=-(g1/.x) by REAL_NS1:4;
A6: (-f1)/.x = -(f1/.x) by A4,VFUNCT_1:def 5;
(-g1)/.x = -(g1/.x) by A2,A4,Def3;
then (-f1).x = (-g1)/.x by A4,A5,A6,PARTFUN1:def 6;
hence (-f1).x = (-g1).x by A2,A4,PARTFUN1:def 6;
end;
-f1 is PartFunc of W,REAL n by REAL_NS1:def 4;
hence -f1 = -g1 by A2,A3,PARTFUN1:5;
end;
theorem Th9:
for f1 be PartFunc of W,REAL-NS n,
g1 be PartFunc of W,REAL n st f1=g1 holds
||. f1 .|| = |. g1 .|
proof
let f1 be PartFunc of W,REAL-NS n,
g1 be PartFunc of W,REAL n;
assume A1: f1=g1;
dom (||. f1 .||) = dom f1 by NORMSP_0:def 3; then
A2: dom (||. f1 .||) = dom(|. g1 .|) by A1,Def2;
now
let x be Element of W;
assume A3: x in dom ||. f1 .||;
A4: f1/.x=g1/.x by A1,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,Def2;
hence (||. f1 .||).x = (|. g1 .|).x by A2,A3,A5,A6,PARTFUN1:def 6;
end;
hence thesis by A2,PARTFUN1:5;
end;
theorem Th10:
for f1,f2 be PartFunc of W,REAL-NS n,
g1,g2 be PartFunc of W,REAL n st f1=g1 & f2=g2 holds
f1-f2 = g1-g2
proof
let f1,f2 be PartFunc of W,REAL-NS n,
g1,g2 be PartFunc of W,REAL n;
assume A1: f1=g1 & f2=g2;
A2: dom(f1-f2) = dom f1 /\ dom f2 by VFUNCT_1:def 2; then
A3: dom(f1-f2) = dom(g1-g2) by A1,VALUED_2:def 46;
A4: now
let x be Element of W;
assume A5: x in dom(f1-f2);
A6: f1/.x=g1/.x & f2/.x=g2/.x by A1,REAL_NS1:def 4;
x in dom f1 & x in dom f2 by A5,A2,XBOOLE_0:def 4; then
g1.x = g1/.x & g2/.x = g2.x by A1,PARTFUN1:def 6; then
A7: f1/.x - f2/.x = g1.x - g2.x by A6,REAL_NS1:5;
A8: (f1-f2)/.x = f1/.x - f2/.x by A5,VFUNCT_1:def 2;
(f1-f2)/.x = (f1-f2).x by A5,PARTFUN1:def 6;
hence (f1-f2).x = (g1-g2).x by A7,A8,A3,A5,VALUED_2:def 46;
end;
f1-f2 is PartFunc of W,REAL n by REAL_NS1:def 4;
hence f1-f2 = g1-g2 by A3,A4,PARTFUN1:5;
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,REAL-NS n such that
A1: f=g & g is_continuous_in x0;
thus x0 in dom f by A1;
let N01 be Subset of REAL n such that
A2: ex r be Real st 0 < r &
{y where y is Element of REAL n: |.y-f/.x0.| < r} = N01;
consider r such that
A3: 0 continuous for 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;
let x0,r;
assume that
A2: x0 in dom f and
A3: 0 continuous for 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:57; then
A2: f is_continuous_in x0 by Def5;
x0 in X by A1,RELAT_1:57;
hence thesis by A2,Th2;
end;
hence thesis;
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:74;
hence thesis by A1;
end;
registration let n;
cluster empty -> continuous for PartFunc of REAL,REAL n;
coherence;
end;
registration let n,f;
let X be trivial set;
cluster f|X -> continuous for PartFunc of REAL,REAL n;
coherence
proof
reconsider g= f as PartFunc of REAL,REAL-NS n
by REAL_NS1:def 4;
g|X is continuous PartFunc of REAL,REAL-NS n;
hence thesis by Th23;
end;
end;
registration let n;
let f1,f2 be continuous PartFunc of REAL,REAL n;
cluster f1+f2 -> continuous for PartFunc of REAL,REAL n;
coherence
proof
reconsider g1= f1,g2=f2 as PartFunc of REAL,REAL-NS n
by REAL_NS1:def 4;
A1: g1 is continuous & g2 is continuous by Th23;
g1+g2= f1+f2 by Th5;
hence thesis by A1,Th23;
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 A1: X c= dom f1 /\ dom f2 & f1|X is continuous & f2|X
is continuous;
reconsider g1=f1,g2=f2 as PartFunc of REAL,REAL-NS n
by REAL_NS1:def 4;
A2: g1|X is continuous by A1,Th23;
g2|X is continuous by A1,Th23; then
A3: (g1+g2) |X is continuous & (g1-g2) |X is continuous
by A1,A2,NFCONT_3:19;
A4: g1+g2 = f1+f2 by Th5;
g1-g2 = f1-f2 by Th10;
hence thesis by A3,A4,Th23;
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 A1: 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,REAL-NS n
by REAL_NS1:def 4;
A2: g1|X is continuous by A1,Th23;
g2|X1 is continuous by A1,Th23; then
A3: (g1+g2) | (X /\ X1) is continuous & (g1-g2) | (X /\ X1) is continuous
by A1,A2,NFCONT_3:20;
A4: g1+g2 = f1+f2 by Th5;
g1-g2 = f1-f2 by Th10;
hence thesis by A3,A4,Th23;
end;
registration let n;
let f be continuous PartFunc of REAL,REAL n;
let r;
cluster r(#)f -> continuous for PartFunc of REAL,REAL n;
coherence
proof
reconsider g= f as PartFunc of REAL,REAL-NS n
by REAL_NS1:def 4;
A1: g is continuous by Th23;
r(#)g = r(#)f by Th6;
hence thesis by A1,Th23;
end;
end;
theorem
X c= dom f & f|X is continuous implies (r(#)f) | X is continuous
proof
assume A1:X c= dom f & f|X is continuous;
reconsider g= f as PartFunc of REAL,REAL-NS n
by REAL_NS1:def 4;
g|X is continuous PartFunc of REAL,REAL-NS n by A1,Th23;
then
A2: (r(#)g) | X is continuous by A1,NFCONT_3:21;
r(#)g = r(#)f by Th6;
hence thesis by A2,Th23;
end;
theorem
X c= dom f & f|X is continuous
implies |. f .| |X is continuous & (-f) | X is continuous
proof
assume A1: X c= dom f & f|X is continuous;
reconsider g= f as PartFunc of REAL,REAL-NS n
by REAL_NS1:def 4;
g|X is continuous by A1,Th23; then
A2: ||. g .|| |X is continuous & (-g) | X is continuous by A1,NFCONT_3:22;
hence |. f .| |X is continuous by Th9;
-g = - f by Th8;
hence (-f) | X is continuous by A2,Th23;
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 A1:
f is total & (for x1,x2 holds f/.(x1+x2) = f/.x1 + f/.x2);
given x0 such that
A2: f is_continuous_in x0;
reconsider g= f as PartFunc of REAL,REAL-NS n
by REAL_NS1:def 4;
A3: now let x1,x2;
A4: 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 A1
.= g/.x1 + g/.x2 by A4,REAL_NS1:2;
end;
g is_continuous_in x0 by A2;
then g|REAL is continuous by A1,A3,NFCONT_3:23;
hence thesis by Th23;
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 A1:dom f is compact & f| (dom f) is continuous & Y = (rng f);
reconsider g= f as PartFunc of REAL,REAL-NS n
by REAL_NS1:def 4;
g| (dom g) is continuous by A1,Th23;
hence Y is compact by A1,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
A1: Y c= dom f & Z = (f.:Y) & Y is compact & f|Y is continuous;
reconsider g = f as PartFunc of REAL,REAL-NS n
by REAL_NS1:def 4;
g|Y is continuous by A1,Th23;
hence Z is compact by A1,NFCONT_3:25;
end;
definition let n,f;
attr f is Lipschitzian means
ex g be PartFunc of REAL,REAL-NS n st g=f & g is Lipschitzian;
end;
theorem Th33:
f is Lipschitzian iff
ex r be Real st 0 Lipschitzian for PartFunc of REAL,REAL n;
coherence
proof
let f be PartFunc of REAL,REAL n;
reconsider g = f as PartFunc of REAL,REAL-NS n
by REAL_NS1:def 4;
assume f is empty;
then g is empty;
hence thesis;
end;
end;
registration let n;
cluster empty for PartFunc of REAL,REAL n;
existence
proof
take the empty PartFunc of REAL,REAL n;
thus thesis;
end;
end;
registration let n;
let f be Lipschitzian PartFunc of REAL,REAL n, X be set;
cluster f|X -> Lipschitzian for PartFunc of REAL,REAL n;
coherence
proof
reconsider g= f as PartFunc of REAL,REAL-NS n
by REAL_NS1:def 4;
g is Lipschitzian by Th34;
then g|X is Lipschitzian;
hence thesis;
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 n;
let f1,f2 be Lipschitzian PartFunc of REAL,REAL n;
cluster f1+f2 -> Lipschitzian for PartFunc of REAL,REAL n;
coherence
proof
reconsider g1=f1,g2=f2 as PartFunc of REAL,REAL-NS n
by REAL_NS1:def 4;
A1:g1 is Lipschitzian & g2 is Lipschitzian by Th34;
g1+g2 = f1+f2 by Th5;
hence thesis by A1;
end;
cluster f1-f2 -> Lipschitzian for PartFunc of REAL,REAL n;
coherence
proof
reconsider g1=f1,g2=f2 as PartFunc of REAL,REAL-NS n
by REAL_NS1:def 4;
A2:g1 is Lipschitzian & g2 is Lipschitzian by Th34;
g1-g2 = f1-f2 by Th10;
hence thesis by A2;
end;
end;
theorem
f1|X is Lipschitzian & f2|X1 is Lipschitzian implies
(f1+f2) | (X /\ X1) is Lipschitzian
proof
assume
A1:f1|X is Lipschitzian & f2|X1 is Lipschitzian;
reconsider g1=f1,g2=f2 as PartFunc of REAL,REAL-NS n
by REAL_NS1:def 4;
g1|X is Lipschitzian & g2|X1 is Lipschitzian by A1; then
A2: (g1+g2) | (X /\ X1) is Lipschitzian by NFCONT_3:28;
g1+g2 = f1+f2 by Th5;
hence thesis by A2;
end;
theorem
f1|X is Lipschitzian & f2|X1 is Lipschitzian implies
(f1-f2) | (X /\ X1) is Lipschitzian
proof
assume
A1:f1|X is Lipschitzian & f2|X1 is Lipschitzian;
reconsider g1=f1,g2=f2 as PartFunc of REAL,REAL-NS n
by REAL_NS1:def 4;
g1|X is Lipschitzian & g2|X1 is Lipschitzian by A1;
then
A2: (g1-g2) | (X /\ X1) is Lipschitzian by NFCONT_3:29;
g1-g2 = f1-f2 by Th10;
hence thesis by A2;
end;
registration let n;
let f be Lipschitzian PartFunc of REAL, REAL n;
let p;
cluster p(#)f -> Lipschitzian for PartFunc of REAL, REAL n;
coherence
proof
reconsider g= f as PartFunc of REAL,REAL-NS n
by REAL_NS1:def 4;
A1: g is Lipschitzian by Th34;
p(#)g = p(#)f by Th6;
hence thesis by A1;
end;
end;
theorem
f|X is Lipschitzian & X c= dom f implies (p(#)f) | X is Lipschitzian
proof
assume A1: f|X is Lipschitzian & X c= dom f;
reconsider g= f as PartFunc of REAL,REAL-NS n
by REAL_NS1:def 4;
A2: (p(#)g) | X is Lipschitzian by A1,NFCONT_3:30;
p(#)g = p(#)f by Th6;
hence thesis by A2;
end;
registration let n;
let f be Lipschitzian PartFunc of REAL, REAL n;
cluster |. f .| -> Lipschitzian for PartFunc of REAL,REAL;
coherence
proof
reconsider g= f as PartFunc of REAL,REAL-NS n
by REAL_NS1:def 4;
g is Lipschitzian by Th34;
then ||. g .|| is Lipschitzian;
hence thesis by Th9;
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;
reconsider g= f as PartFunc of REAL,REAL-NS n
by REAL_NS1:def 4;
g|X is Lipschitzian by A1; then
A2: -(g|X) is Lipschitzian & (||. g .||) |X is Lipschitzian &
(-g) | X is Lipschitzian by NFCONT_3:31;
-(g|X) = -(f|X) by Th8;
hence -(f|X) is Lipschitzian by A2;
thus (|. f .|) |X is Lipschitzian by A2,Th9;
-g = - f by Th8;
hence thesis by A2;
end;
registration let n;
cluster constant -> Lipschitzian for 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,REAL-NS n
by REAL_NS1:def 4;
g is constant by A1;
hence thesis;
end;
end;
registration let n;
cluster Lipschitzian -> continuous for PartFunc of REAL, REAL n;
coherence
by Th23;
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 A1: for x0 st x0 in X holds f/.x0 = x0*r+p;
reconsider g= f as PartFunc of REAL,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 A2: x0 in X;
A3: x0*r = x0*r0 by REAL_NS1:3;
thus g/.x0 = f/.x0 by REAL_NS1:def 4
.= x0*r+p by A2,A1
.= x0*r0+p0 by A3,REAL_NS1:2;
end;
then g|X is continuous by NFCONT_3:33;
hence thesis by Th23;
end;
theorem Th42:
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 A1: 1 <=i & i <= n;
A2:dom proj(i,n) = REAL n by FUNCT_2:def 1;
reconsider prg=proj(i,n) as PartFunc of REAL-NS n,REAL
by REAL_NS1:def 4;
reconsider px0 = x0 as Element of REAL-NS n
by REAL_NS1:def 4;
now let r be Real;
assume A3: 0