:: More on the Continuity of Real Functions
:: by Keiko Narita , Artur Kornilowicz and Yasunari Shidama
::
:: Received February 22, 2011
:: Copyright (c) 2011-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, SEQ_1, PARTFUN1, RELAT_1, TARSKI, SEQ_2,
ORDINAL2, FUNCT_2, FUNCT_1, XBOOLE_0, XXREAL_0, NAT_1, ARYTM_3, CARD_1,
COMPLEX1, ARYTM_1, REAL_1, RCOMP_1, 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<r ex s st 0<s & for x1 st x1 in dom f & |.x1-x0.|<s
holds |. f/.x1 - f/.x0 .|<r
proof
hereby 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;
thus
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 r;
assume 0<r;
then consider s such that
A2: 0<s & for x1 st x1
in dom g & |.x1-x0.|<s holds ||. g/.x1 - g/.x0 .||<r by A1,NFCONT_3:8;
take s;
thus 0 < s by A2;
let x1;
assume x1 in dom f & |.x1-x0.|<s; then
A3: ||. g/.x1 - g/.x0 .|| < r by A1,A2;
g/.x1 = f/.x1 & g/.x0 = f/.x0 by A1,REAL_NS1:def 4;
hence |. f/.x1 - f/.x0 .|<r by A3,REAL_NS1:1,5;
end;
end;
assume
A4: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;
reconsider g= f as PartFunc of REAL,REAL-NS n
by REAL_NS1:def 4;
now let r be Real;
reconsider rr=r as Real;
assume 0<r;
then consider s such that
A5: 0<s and
A6: for x1 st x1 in dom f & |.x1-x0.|<s holds |. f/.x1 - f/.x0 .|<rr by A4;
take s;
thus 0<s by A5;
let x1;
assume x1 in dom g & |.x1-x0.|<s; then
A7: |. f/.x1 - f/.x0 .|<r by A6;
g/.x1 = f/.x1 & g/.x0 = f/.x0 by REAL_NS1:def 4;
hence ||. g/.x1 - g/.x0 .||<r by A7,REAL_NS1:1,5;
end;
then g is_continuous_in x0 by A4,NFCONT_3:8;
hence thesis;
end;
theorem Th4:
for r be Real, z be Element of REAL n,w be Point of REAL-NS n
st z=w holds
{y where y is Element of REAL n: |.y-z.| < r} =
{y where y is Point of REAL-NS n: ||.y-w.|| < r}
proof
let r be Real, z be Element of REAL n,w be Point of REAL-NS n;
assume A1: z=w;
set N1={y where y is Element of REAL n: |.y-z.| < r};
set N2={y where y is Point of REAL-NS n: ||.y-w.|| < r};
A2: N1 c= N2
proof let x be object;
assume x in N1;
then consider y be Element of REAL n such that
A3: x=y & |.y-z.| < r;
reconsider x1=x as Element of REAL n by A3;
reconsider x2=x1 as Point of REAL-NS n by REAL_NS1:def 4;
||.x2-w.|| < r by A1,A3,REAL_NS1:1,5;
hence x in N2;
end;
N2 c= N1
proof let x be object;
assume x in N2;
then consider y be Point of REAL-NS n such that
A4: x=y & ||.y-w.|| < r;
reconsider x3=x as Point of REAL-NS n by A4;
reconsider x4=x3 as Element of REAL n by REAL_NS1:def 4;
|.x4-z.| < r by A1,A4,REAL_NS1:1,5;
hence x in N1;
end;
hence N1 = N2 by A2,XBOOLE_0:def 10;
end;
definition
let n be Element of NAT;
let Z be set;
let f be PartFunc of Z,REAL n;
deffunc F(object) = |. f/.$1 .|;
func |.f.| -> 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<r and
A4: { p where p is Element of REAL n : |. p - f/.x0 .| < r } = N01 by A2;
f/.x0 = g/.x0 by A1,REAL_NS1:def 4; then
A5: { p where p is Point of REAL-NS n : ||. p - g/.x0 .|| < r } = N01
by A4,Th4;
{ p where p is Point of REAL-NS n : ||. p - g/.x0 .|| < r }
is Neighbourhood of g/.x0 by A3,NFCONT_1:3;
then consider N being Neighbourhood of x0 such that
A6: for x1 st x1 in dom g & x1 in N holds g/.x1 in N01 by A5,A1,NFCONT_3:9;
take N;
let x1;
assume x1 in dom f & x1 in N;
then g/.x1 in N01 by A1,A6;
hence f/.x1 in N01 by A1,REAL_NS1:def 4;
end;
assume
A7: 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;
reconsider g= f as PartFunc of REAL,REAL-NS n
by REAL_NS1:def 4;
now let N1 being Neighbourhood of g/.x0;
consider r be Real such that
A8: 0<r and
A9: { p where p is Point of REAL-NS n : ||. p - g/.x0 .|| < r } c= N1
by NFCONT_1:def 1;
reconsider rr=r as Real;
A10: 0 < rr by A8;
set N01 = { p where p is Element of REAL n : |. p - f/.x0 .| < r };
f/.x0 = g/.x0 by REAL_NS1:def 4; then
A11: { p where p is Element of REAL n : |. p - f/.x0 .| < r }
= { p where p is Point of REAL-NS n : ||. p - g/.x0 .|| < r } by Th4;
now let x be object;
assume x in N01;
then ex p be Element of REAL n
st p=x & |. p - f/.x0 .| < r;
hence x in REAL n;
end;
then N01 is Subset of REAL n by TARSKI:def 3;
then consider N being Neighbourhood of x0 such that
A12: for x1 st x1 in dom f & x1 in N holds f/.x1 in N01 by A7,A10;
take N;
let x1;
assume x1 in dom g & x1 in N;
then f/.x1 in N01 by A12;
then g/.x1 in N01 by REAL_NS1:def 4;
hence g/.x1 in N1 by A9,A11;
end;
then g is_continuous_in x0 by A7,NFCONT_3:9;
hence thesis;
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 f.:N c= N1
proof
reconsider g= f as PartFunc of REAL,REAL-NS n
by REAL_NS1:def 4;
hereby assume f is_continuous_in x0; then
A1: g is_continuous_in x0;
hence x0 in dom f;
thus 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 f.:N c= N1
proof
let N1 be Subset of REAL n;
given r be Real such that
A2: 0 < r & {y where y is Element of REAL n: |.y-f/.x0.| < r} = N1;
f/.x0 = g/.x0 by REAL_NS1:def 4; then
A3: { p where p is Element of REAL n : |. p - f/.x0 .| < r }
= { p where p is Point of REAL-NS n : ||. p - g/.x0 .|| < r } by Th4;
N1 is Neighbourhood of g/.x0 by A2,A3,NFCONT_1:3;
then consider N being Neighbourhood of x0 such that
A4: g.:N c= N1 by A1,NFCONT_3:10;
take N;
thus f.:N c= N1 by A4;
end;
end;
assume A5: 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 f.:N c= N1;
now let N1 being Neighbourhood of g/.x0;
consider r be Real such that
A6: 0<r and
A7: { p where p is Point of REAL-NS n : ||. p - g/.x0 .|| < r } c= N1
by NFCONT_1:def 1;
reconsider rr=r as Real;
A8: 0<rr by A6;
set N01={ p where p is Element of REAL n : |. p - f/.x0 .| < r };
f/.x0 = g/.x0 by REAL_NS1:def 4; then
A9: { p where p is Element of REAL n: |. p - f/.x0 .| < r }
= { p where p is Point of REAL-NS n : ||. p - g/.x0 .|| < r } by Th4;
now let x be object;
assume x in N01;
then ex p be Element of REAL n st p=x & |. p - f/.x0 .| < r;
hence x in REAL n;
end;
then N01 is Subset of REAL n by TARSKI:def 3;
then consider N being Neighbourhood of x0 such that
A10: f.:N c= N01 by A5,A8;
take N;
thus g.:N c= N1 by A7,A9,A10;
end;
then g is_continuous_in x0 by A5,NFCONT_3:10;
hence thesis;
end;
theorem
(ex N be Neighbourhood of x0 st dom f /\ N = {x0}) implies
f is_continuous_in x0
proof
given N be Neighbourhood of x0 such that
A1: dom f /\ N = {x0};
reconsider g = f as PartFunc of REAL,REAL-NS n
by REAL_NS1:def 4;
g is_continuous_in x0 by A1,NFCONT_3:11;
hence thesis;
end;
theorem
x0 in dom f1 /\ dom f2 & f1 is_continuous_in x0 & f2 is_continuous_in x0
implies f1+f2 is_continuous_in x0
proof
assume A1: x0 in dom f1 /\ dom f2 & f1 is_continuous_in x0
& f2 is_continuous_in x0;
reconsider g1=f1, g2=f2 as PartFunc of REAL,REAL-NS n
by REAL_NS1:def 4;
A2: (g1+g2) is_continuous_in x0 & (g1-g2) is_continuous_in x0
by A1,NFCONT_3:12;
g1+g2 = f1+f2 by Th5;
hence thesis by A2;
end;
theorem
x0 in dom f1 /\ dom f2 & f1 is_continuous_in x0 & f2 is_continuous_in x0
implies f1-f2 is_continuous_in x0
proof
assume A1: x0 in dom f1 /\ dom f2 & f1 is_continuous_in x0 &
f2 is_continuous_in x0;
reconsider g1=f1,g2=f2 as PartFunc of REAL,REAL-NS n
by REAL_NS1:def 4;
A2:(g1+g2) is_continuous_in x0 & (g1-g2) is_continuous_in x0
by A1,NFCONT_3:12;
g1-g2 = f1-f2 by Th10;
hence thesis by A2;
end;
theorem
f is_continuous_in x0 implies r(#)f is_continuous_in x0
proof
assume A1:f is_continuous_in x0;
reconsider g = f as PartFunc of REAL,REAL-NS n
by REAL_NS1:def 4;
g is_continuous_in x0 by A1; then
A2: r(#)g is_continuous_in x0 by NFCONT_3:13;
r(#)g = r(#)f by Th6;
hence thesis by A2;
end;
theorem
x0 in dom f & f is_continuous_in x0 implies
|. f .| is_continuous_in x0
proof
assume
A1: x0 in dom f & f is_continuous_in x0;
reconsider g = f as PartFunc of REAL,REAL-NS n
by REAL_NS1:def 4;
g is_continuous_in x0 by A1;
then ||. g .|| is_continuous_in x0 by NFCONT_3:14;
hence thesis by Th9;
end;
theorem
x0 in dom f & f is_continuous_in x0 implies
-f is_continuous_in x0
proof
assume
A1: x0 in dom f & f is_continuous_in x0;
reconsider g = f as PartFunc of REAL,REAL-NS n
by REAL_NS1:def 4;
g is_continuous_in x0 by A1; then
A2: -g is_continuous_in x0 by NFCONT_3:14;
-g = -f by Th8;
hence thesis by A2;
end;
theorem
for S be RealNormSpace,
z be Point of REAL-NS n,
f1 be PartFunc of REAL,REAL n,
f2 be PartFunc of REAL-NS n,S
st x0 in dom (f2*f1) & f1 is_continuous_in x0
& z=f1/.x0 & f2 is_continuous_in z
holds f2*f1 is_continuous_in x0
proof
let S be RealNormSpace,
z be Point of REAL-NS n,
f1 be PartFunc of REAL,REAL n,
f2 be PartFunc of REAL-NS n,S;
assume A1: x0 in dom (f2*f1) & f1 is_continuous_in x0
& z=f1/.x0 & f2 is_continuous_in z;
reconsider g1= f1 as PartFunc of REAL,REAL-NS n
by REAL_NS1:def 4;
f1/.x0 = g1/.x0 by REAL_NS1:def 4;
hence thesis by A1,NFCONT_3:15;
end;
theorem Th20:
for S be RealNormSpace,
f1 be PartFunc of REAL,S,
f2 be PartFunc of S,REAL
st x0 in dom (f2*f1) & f1 is_continuous_in x0
& f2 is_continuous_in f1/.x0
holds f2*f1 is_continuous_in x0
proof
let S be RealNormSpace,
f1 be PartFunc of REAL,S,
f2 be PartFunc of S,REAL;
assume
A1: x0 in dom (f2*f1);
assume that
A2: f1 is_continuous_in x0 and
A3: f2 is_continuous_in f1/.x0;
let s1 be Real_Sequence such that
A4: rng s1 c= dom (f2*f1) and
A5: s1 is convergent & lim s1 = x0;
A6: dom (f2*f1) c= dom f1 by RELAT_1:25;
A7: rng (f1/*s1) c= dom f2
proof
let x be object;
assume x in rng (f1/*s1);
then consider n such that
A8: x=(f1/*s1).n by FUNCT_2:113;
s1.n in rng s1 by VALUED_0:28;
then f1.(s1.n) in dom f2 by A4,FUNCT_1:11;
hence x in dom f2 by A4,A6,A8,FUNCT_2:108,XBOOLE_1:1;
end;
A9: now
let n;
s1.n in rng s1 by VALUED_0:28; then
A10: s1.n in dom f1 by A4,FUNCT_1:11;
thus ((f2*f1)/*s1).n = (f2*f1).(s1.n) by A4,FUNCT_2:108
.= f2.(f1.(s1.n)) by A10,FUNCT_1:13
.= f2.((f1/*s1).n) by A4,A6,FUNCT_2:108,XBOOLE_1:1
.= (f2/*(f1/*s1)).n by A7,FUNCT_2:108;
end; then
A11: f2/*(f1/*s1) = (f2*f1)/*s1 by FUNCT_2:63;
rng s1 c= dom f1 by A4,A6; then
A12: f1/*s1 is convergent & f1/.x0 = lim (f1/*s1) by A2,A5;
hence (f2*f1)/*s1 is convergent by A3,A7,A11,NFCONT_1:def 6;
thus (f2*f1).x0 = (f2*f1)/.x0 by A1,PARTFUN1:def 6
.=f2/.(f1/.x0) by A1,PARTFUN2:3
.= lim (f2/*(f1/*s1)) by A12,A3,A7,NFCONT_1:def 6
.= lim ((f2*f1)/*s1) by A9,FUNCT_2:63;
end;
definition let n;
let f be PartFunc of REAL n,REAL;
let x0 be Element of REAL n;
pred f is_continuous_in x0 means
ex y0 be Point of REAL-NS n, g be PartFunc of REAL-NS n,REAL st
x0=y0 & f=g & g is_continuous_in y0;
end;
theorem
for f be PartFunc of REAL n,REAL,
h be PartFunc of REAL-NS n,REAL,
x0 be Element of REAL n,
y0 be Point of REAL-NS n
st f=h & x0=y0 holds
f is_continuous_in x0 iff h is_continuous_in y0;
theorem Th22:
for f1 be PartFunc of REAL,REAL n,
f2 be PartFunc of REAL n,REAL st x0 in dom (f2*f1) &
f1 is_continuous_in x0 & f2 is_continuous_in f1/.x0
holds f2*f1 is_continuous_in x0
proof
let f1 be PartFunc of REAL,REAL n,
f2 be PartFunc of REAL n,REAL;
assume
A1: x0 in dom (f2*f1) & f1 is_continuous_in x0
& f2 is_continuous_in f1/.x0;
reconsider g1=f1 as PartFunc of REAL,REAL-NS n
by REAL_NS1:def 4;
reconsider g2=f2 as PartFunc of REAL-NS n,REAL
by REAL_NS1:def 4;
f1/.x0 = g1/.x0 by REAL_NS1:def 4;
then g2 is_continuous_in g1/.x0 by A1;
hence thesis by A1,Th20;
end;
definition let n,f;
attr f is continuous means :Def5:
for x0 st x0 in dom f holds f is_continuous_in x0;
end;
theorem Th23:
for g be PartFunc of REAL,REAL-NS n,
f be PartFunc of REAL,REAL n st g=f holds
g is continuous iff f is continuous
proof
let g be PartFunc of REAL,REAL-NS n,
f be PartFunc of REAL,REAL n;
assume A1: g=f;
hereby assume g is continuous;
then for x0 st x0 in dom f holds f is_continuous_in x0 by A1;
hence f is continuous;
end;
assume
A2: f is continuous;
now
let x0;
assume x0 in dom g;
then f is_continuous_in x0 by A2,A1;
hence g is_continuous_in x0 by A1;
end;
hence thesis;
end;
theorem Th24:
X c= dom f implies
(f|X is continuous iff for x0,r st x0 in X & 0<r
ex s st 0<s & for x1 st x1 in X & |.x1-x0.| < s
holds |. f/.x1 - f/.x0 .| < r)
proof
assume
A1: X c= dom f;
thus f|X is continuous implies for x0,r st x0 in X & 0<r ex s st 0<s & for
x1 st x1 in X & |.x1-x0.| < s holds |. f/.x1 - f/.x0 .| < r
proof
assume
A2: f|X is continuous;
let x0,r;
assume that
A3: x0 in X and
A4: 0<r;
x0 in dom(f|X) by A1,A3,RELAT_1:62;
then f|X is_continuous_in x0 by A2;
then consider s such that
A5: 0<s and
A6: for x1 st x1 in dom(f|X) & |.x1-x0.|<s
holds |.(f|X)/.x1-(f|X)/.x0 .| <r by A4,Th3;
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 RELAT_1:61
.= X by A1,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
A10: 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;
A11: dom (f|X) = dom f /\ X by RELAT_1:61
.= X by A1,XBOOLE_1:28;
now
let x0 such that
A12: x0 in dom(f|X);
A13: x0 in X by A12,RELAT_1:57;
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 A10,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,PARTFUN2:15
.= |. f/.x1 - f/.x0 .| by A16,PARTFUN2:15;
hence thesis by A11,A15,A16,A17;
end;
hence f|X is_continuous_in x0 by Th3,A12;
end;
hence thesis;
end;
registration let n;
cluster constant -> 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<r;
take s;
thus 0<s;
let x1;
assume
A4: x1 in dom f;
assume |.x1-x0.| < s;
f/.x1 =f.x1 by A4,PARTFUN1:def 6
.=f.x0 by A1,A2,A4,FUNCT_1:def 10
.= f/.x0 by A2,PARTFUN1:def 6;
hence |. f/.x1 - f/.x0 .| < r by A3;
end;
then f|dom f is continuous by Th24;
hence thesis by RELAT_1:69;
end;
end;
registration let n;
cluster continuous for PartFunc of REAL,REAL n;
existence
proof
take f = the constant PartFunc of REAL,REAL n;
thus thesis;
end;
end;
registration let n;
let f be continuous PartFunc of REAL,REAL n, X be set;
cluster f|X -> 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<r & for x1,x2 st x1 in dom f &
x2 in dom f holds |.f/.x1-f/.x2.| <= r*|.x1-x2.|
proof
hereby assume f is Lipschitzian;
then
consider g be PartFunc of REAL,REAL-NS n such that
A1: g=f & g is Lipschitzian;
consider r be Real such that
A2: 0<r & for x1,x2 st x1 in dom g &
x2 in dom g holds ||.g/.x1-g/.x2.||<=r*|.x1-x2.| by A1;
take r;
thus 0<r by A2;
thus for x1,x2 st x1 in dom f &
x2 in dom f holds |.f/.x1-f/.x2.|<=r*|.x1-x2.|
proof
let x1,x2;
assume x1 in dom f & x2 in dom f; then
A3: ||.g/.x1-g/.x2.||<=r*|.x1-x2.| by A1,A2;
f/.x1 = g/.x1 & f/.x2 = g/.x2 by A1,REAL_NS1:def 4;
hence |.f/.x1-f/.x2.|<=r*|.x1-x2.| by A3,REAL_NS1:1,5;
end;
end;
given r be Real such that
A4: 0<r & for x1,x2 st x1 in dom f &
x2 in dom f holds |.f/.x1-f/.x2.|<=r*|.x1-x2.|;
reconsider g= f as PartFunc of REAL,REAL-NS n
by REAL_NS1:def 4;
now
let x1,x2;
assume x1 in dom g & x2 in dom g; then
A5: |.f/.x1-f/.x2.|<=r*|.x1-x2.| by A4;
f/.x1 = g/.x1 & f/.x2 = g/.x2 by REAL_NS1:def 4;
hence ||.g/.x1-g/.x2.||<=r*|.x1-x2.| by A5,REAL_NS1:1,5;
end;
then g is Lipschitzian by A4;
hence thesis;
end;
theorem Th34:
f=h implies (f is Lipschitzian iff h is Lipschitzian);
theorem
f|X is Lipschitzian iff ex r be Real
st 0<r & for x1,x2 st x1 in dom(f|X) &
x2 in dom(f|X) holds |. f/.x1-f/.x2 .| <= r*|.x1-x2.|
proof
hereby assume f|X is Lipschitzian; then
consider r be Real such that
A1: 0<r & for x1,x2 st x1 in dom (f|X) &
x2 in dom (f|X) holds |.(f|X)/.x1-(f|X)/.x2.|<=r*|.x1-x2.| by Th33;
take r;
thus 0<r by A1;
thus for x1,x2 st x1 in dom(f|X) &
x2 in dom(f|X) holds |. f/.x1-f/.x2 .|<=r*|.x1-x2.|
proof
let x1,x2;
assume A2: x1 in dom(f|X) & x2 in dom(f|X); then
|.(f|X)/.x1-(f|X)/.x2.|<=r*|.x1-x2.| by A1; then
|.f/.x1-(f|X)/.x2.|<=r*|.x1-x2.| by A2,PARTFUN2:15;
hence |.f/.x1-f/.x2.|<=r*|.x1-x2.| by A2,PARTFUN2:15;
end;
end;
given r be Real such that
A3: 0<r & for x1,x2 st x1 in dom(f|X) &
x2 in dom(f|X) holds |. f/.x1-f/.x2 .|<=r*|.x1-x2.|;
now
let x1,x2;
assume A4: x1 in dom(f|X) & x2 in dom(f|X);
then |. f/.x1-f/.x2 .|<=r*|.x1-x2.| by A3;
then |.(f|X)/.x1-f/.x2.|<=r*|.x1-x2.| by A4,PARTFUN2:15;
hence |.(f|X)/.x1-(f|X)/.x2.|<=r*|.x1-x2.| by A4,PARTFUN2:15;
end;
hence f|X is Lipschitzian by A3,Th33;
end;
registration let n;
cluster empty -> 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<r;
take s = r;
thus 0<s by A3;
now let px1 be Element of REAL-NS n;
assume A4: px1 in dom prg & ||.px1-px0.|| < r;
reconsider x1=px1 as Element of REAL n by REAL_NS1:def 4;
A5: ||.px1-px0.|| = |.x1-x0.| by REAL_NS1:1,5;
proj(i,n)/.(x1-x0) =proj(i,n)/.x1-proj(i,n)/.x0 by A1,PDIFF_8:12;
then |. proj(i,n)/.x1-proj(i,n)/.x0.| <= |. x1-x0 .|
by A1,PDIFF_8:5;
hence |. proj(i,n)/.px1-proj(i,n)/.px0.| < r by A4,A5,XXREAL_0:2;
end;
hence for px1 be Element of REAL-NS n st px1 in dom prg
& ||.px1-px0.|| < s holds |. proj(i,n)/.px1-proj(i,n)/.px0 .|<r;
end;
then prg is_continuous_in px0 by A2,NFCONT_1:8;
hence thesis;
end;
theorem Th43:
for n be non zero Element of NAT, h be PartFunc of REAL, REAL n holds
h is_continuous_in x0 iff
(x0 in dom h & for i be Element of NAT st i in Seg n
holds proj(i,n)*h is_continuous_in x0)
proof
let n be non zero Element of NAT, h be PartFunc of REAL,REAL n;
hereby
assume A1: h is_continuous_in x0;
hence
A2: x0 in dom h by Th3;
thus for i be Element of NAT st i in Seg n
holds proj(i,n)*h is_continuous_in x0
proof
let i be Element of NAT;
assume i in Seg n; then
A3: 1<=i & i <= n by FINSEQ_1:1;
A4:dom (proj(i,n)) = REAL n by FUNCT_2:def 1;
rng h c= REAL n; then
A5: dom (proj(i,n)*h) = dom h by A4,RELAT_1:27;
proj(i,n) is_continuous_in h/.x0 by A3,Th42;
hence thesis by A5,A1,A2,Th22;
end;
end;
assume
A6: x0 in dom h &
for i be Element of NAT st i in Seg n
holds (proj(i,n)*h) is_continuous_in x0;
for r be Real st 0<r ex s be Real
st 0<s & for x1 be Real st x1
in dom h & |.x1-x0.|<s holds |. h/.x1 - h/.x0 .|<r
proof
let r0 be Real;
assume A7: 0 < r0;
set r=r0/2;
A8:0 < r by A7,XREAL_1:215;
defpred P[Nat,Real] means 0 < $2 &
for x1 be Real st x1 in dom h & |.x1-x0.| < $2 holds
|. (proj($1,n)*h).x1 - (proj($1,n)*h).x0 .| < r/n;
A9: 0 < r/n by A8,XREAL_1:139;
A10: for j be Nat st j in Seg n ex x be Element of REAL st P[j,x]
proof
let j be Nat;
assume A11: j in Seg n;
A12: proj(j,n)*h is_continuous_in x0 by A6,A11;
A13:dom (proj(j,n)) = REAL n by FUNCT_2:def 1;
rng h c= REAL n; then
A14:dom (proj(j,n)*h) = dom h by A13,RELAT_1:27;
consider sj be Real such that
A15: 0 < sj &
for x1 be Real st x1 in dom (proj(j,n)*h) & |.x1-x0.| < sj holds
|.(proj(j,n)*h).x1 - (proj(j,n)*h).x0 .| < r/n by A12,A9,FCONT_1:3;
sj in REAL by XREAL_0:def 1;
hence thesis by A15,A14;
end;
consider s0 be FinSequence of REAL such that
A16: dom s0 = Seg n &
for k be Nat st k in Seg n holds P[k,s0.k] from FINSEQ_1:sch 5(A10);
n in Seg n by FINSEQ_1:3;
then reconsider rs0= rng s0 as non empty ext-real-membered set
by A16,FUNCT_1:3;
rng s0 is finite by A16,FINSET_1:8;
then reconsider rs0 as left_end right_end non empty ext-real-membered set;
A17:min rs0 in rng s0 by XXREAL_2:def 7;
reconsider s = min rs0 as Real;
take s;
ex i1 be object st i1 in dom s0 & s = s0.i1 by A17,FUNCT_1:def 3;
hence 0 < s by A16;
now let x1;
assume A18: x1 in dom h & |.x1- x0.| < s;
now let j be Element of NAT;
assume 1<=j & j <= n; then
A19: j in Seg n by FINSEQ_1:1;
then s0.j in rng s0 by A16,FUNCT_1:3;
then s <= s0.j by XXREAL_2:def 7;
then |.x1-x0.| < s0.j by A18,XXREAL_0:2; then
A20: |. (proj(j,n)*h).x1 - (proj(j,n)*h).x0 .| < r/n by A19,A18,A16;
A21:(proj(j,n)*h).x1 =(proj(j,n)).(h.x1) by A18,FUNCT_1:13
.=(proj(j,n)).(h/.x1) by A18,PARTFUN1:def 6;
(proj(j,n)*h).x0 = (proj(j,n)).(h.x0) by A6,FUNCT_1:13
.=(proj(j,n)).(h/.x0) by A6,PARTFUN1:def 6;
hence |. proj(j,n).((h/.x1) - (h/.x0)) .| <= r/n by A20,A21,PDIFF_8:12;
end;
then |. h/.x1 - h/.x0 .| <= n*(r/n) by PDIFF_8:17; then
A22: |. h/.x1 - h/.x0 .| <= r by XCMPLX_1:87;
r < r0 by A7,XREAL_1:216;
hence|. h/.x1 - h/.x0 .| < r0 by A22,XXREAL_0:2;
end;
hence for x1 st x1 in dom h & |.x1-x0.| < s
holds |. h/.x1 - h/.x0 .| < r0;
end;
hence thesis by A6,Th3;
end;
theorem
for n be non zero Element of NAT, h be PartFunc of REAL, REAL n holds
h is continuous iff
for i be Element of NAT st i in Seg n
holds proj(i,n)*h is continuous
proof
let n be non zero Element of NAT,
h be PartFunc of REAL, REAL n;
hereby assume
A1: h is continuous;
thus for i be Element of NAT st i in Seg n holds (proj(i,n)*h) is continuous
proof
let i be Element of NAT;
assume A2: i in Seg n;
A3:dom (proj(i,n)) = REAL n by FUNCT_2:def 1;
rng h c= REAL n; then
A4:dom (proj(i,n)*h) = dom h by A3,RELAT_1:27;
now let x0;
assume x0 in dom (proj(i,n)*h);
then h is_continuous_in x0 by A1,A4;
hence (proj(i,n)*h) is_continuous_in x0 by A2,Th43;
end;
hence proj(i,n)*h is continuous;
end;
end;
assume
A5: for i be Element of NAT st i in Seg n holds (proj(i,n)*h) is continuous;
let x0;
assume A6: x0 in dom h;
now let i be Element of NAT;
assume A7: i in Seg n;
A8:dom (proj(i,n)) = REAL n by FUNCT_2:def 1;
rng h c= REAL n; then
A9:dom (proj(i,n)*h) = dom h by A8,RELAT_1:27;
(proj(i,n)*h) is continuous by A5,A7;
hence (proj(i,n)*h) is_continuous_in x0 by A6,A9;
end;
hence thesis by A6,Th43;
end;
theorem Th45:
for x0 be Point of REAL-NS n st 1 <= i & i <= n holds
Proj(i,n) is_continuous_in x0
proof
let x0 be Point of REAL-NS n;
assume A1: 1 <= i & i <= n;
A2: dom (Proj(i,n)) = the carrier of REAL-NS n by FUNCT_2:def 1;
now let r be Real;
assume A3: 0<r;
take s = r;
thus 0< s by A3;
now let x1 be Point of REAL-NS n;
assume A4: x1 in dom (Proj(i,n)) & ||.x1-x0.|| < s;
Proj(i,n)/.(x1-x0) = Proj(i,n)/.x1-Proj(i,n)/.x0 by A1,PDIFF_8:11;
then ||. Proj(i,n)/.x1-Proj(i,n)/.x0.|| <= ||. x1-x0 .||
by A1,PDIFF_8:3;
hence ||. Proj(i,n)/.x1-Proj(i,n)/.x0.|| < r by A4,XXREAL_0:2;
end;
hence for x1 be Point of REAL-NS n st x1 in dom (Proj(i,n))
& ||.x1-x0.|| < s holds ||. Proj(i,n)/.x1-Proj(i,n)/.x0 .||<r;
end;
hence thesis by A2,NFCONT_1:7;
end;
theorem Th46:
for n be non zero Element of NAT,
h be PartFunc of REAL,REAL-NS n holds
h is_continuous_in x0 iff
for i be Element of NAT st i in Seg n
holds Proj(i,n)*h is_continuous_in x0
proof
let n be non zero Element of NAT,
h be PartFunc of REAL, REAL-NS n;
hereby assume A1: h is_continuous_in x0;
thus for i be Element of NAT st i in Seg n
holds Proj(i,n)*h is_continuous_in x0
proof
let i be Element of NAT;
assume i in Seg n; then
A2: 1<=i & i <= n by FINSEQ_1:1;
A3:dom (Proj(i,n)) = the carrier of REAL-NS n by FUNCT_2:def 1;
rng h c= the carrier of REAL-NS n; then
A4: dom (Proj(i,n)*h) = dom h by A3,RELAT_1:27;
Proj(i,n) is_continuous_in h/.x0 by A2,Th45;
hence (Proj(i,n)*h) is_continuous_in x0 by A4,A1,NFCONT_3:15;
end;
end;
assume A5: for i be Element of NAT st i in Seg n
holds (Proj(i,n)*h) is_continuous_in x0;
1<=n by NAT_1:14;
then 1 in Seg n by FINSEQ_1:1;
then (Proj(1,n)*h) is_continuous_in x0 by A5; then
A6:x0 in dom(Proj(1,n)*h);
A7:dom(Proj(1,n)*h) c= dom h by RELAT_1:25;
for r being Real st 0<r ex s st 0<s & for x1 st x1
in dom h & |.x1-x0.|<s holds ||. h/.x1 - h/.x0 .||<r
proof
let r0 be Real;
set r=r0/2;
assume A8: 0 < r0; then
A9:0 < r by XREAL_1:215;
defpred P[set,Real] means
ex j be Element of NAT st $1=j & 0 < $2 &
for x1 st x1 in dom h & |.x1-x0.| < $2 holds
||. (Proj(j,n)*h)/.x1 - (Proj(j,n)*h)/.x0 .|| < r/n;
A10: 0 < r/n by A9,XREAL_1:139;
A11: for j0 be Nat st j0 in Seg n holds
ex x be Element of REAL st P[j0,x]
proof
let j0 be Nat;
assume A12: j0 in Seg n;
reconsider j=j0 as Element of NAT by ORDINAL1:def 12;
A13: Proj(j,n)*h is_continuous_in x0 by A5,A12;
A14:dom (Proj(j,n)) = the carrier of REAL-NS n by FUNCT_2:def 1;
rng h c= the carrier of REAL-NS n; then
A15:dom (Proj(j,n)*h) = dom h by A14,RELAT_1:27;
consider sj be Real such that
A16: 0 < sj &
for x1 st x1 in dom (Proj(j,n)*h) & |.x1-x0.| < sj holds
||. (Proj(j,n)*h)/.x1 - (Proj(j,n)*h)/.x0 .|| < r/n by A13,A10,NFCONT_3:8;
sj in REAL by XREAL_0:def 1;
hence thesis by A16,A15;
end;
consider s0 be FinSequence of REAL such that
A17: dom s0 = Seg n &
for k be Nat st k in Seg n holds P[k,s0.k] from FINSEQ_1:sch 5(A11);
n in Seg n by FINSEQ_1:3;
then reconsider rs0= rng s0 as non empty ext-real-membered set
by A17,FUNCT_1:3;
rng s0 is finite by A17,FINSET_1:8;
then reconsider rs0 as left_end right_end non empty ext-real-membered set;
A18:min rs0 in rng s0 by XXREAL_2:def 7;
reconsider s = min rs0 as Real;
take s;
consider i1 be object such that
A19: i1 in dom s0 & s = s0.i1 by A18,FUNCT_1:def 3;
ex j be Element of NAT st i1=j & 0 < s0.i1 &
for x1 st x1 in dom h & |.x1-x0.| < s0.i1 holds
||. (Proj(j,n)*h)/.x1 - (Proj(j,n)*h)/.x0 .|| < r/n by A17,A19;
hence 0 < s by A19;
let x1;
assume A20: x1 in dom h & |.x1-x0.| < s;
now let j be Element of NAT;
assume 1<=j & j <= n; then
A21:j in Seg n by FINSEQ_1:1;
then consider jj be Element of NAT such that
A22: jj = j & 0 < s0.j &
for x1 st x1 in dom h & |.x1-x0.|< s0.j holds
||. (Proj(jj,n)*h)/.x1 - (Proj(jj,n)*h)/.x0 .|| < r/n by A17;
s0.j in rng s0 by A21,A17,FUNCT_1:3;
then s <= s0.j by XXREAL_2:def 7;
then |.x1-x0.| < s0.j by A20,XXREAL_0:2; then
A23: ||. (Proj(j,n)*h)/.x1 - (Proj(j,n)*h)/.x0 .|| < r/n by A22,A20;
A24:dom (Proj(j,n)) = the carrier of REAL-NS n by FUNCT_2:def 1; then
A25:(Proj(j,n)*h)/.x1 = (Proj(j,n))/.(h/.x1) by A20,PARTFUN2:4;
(Proj(j,n)*h)/.x0 = (Proj(j,n))/.(h/.x0) by A24,A7,A6,PARTFUN2:4;
hence ||. Proj(j,n).((h/.x1) - (h/.x0)) .|| <= r/n
by A23,A25,PDIFF_8:11;
end;
then ||. h/.x1 - h/.x0 .|| <= n*(r/n) by PDIFF_8:16; then
A26: ||. h/.x1 - h/.x0 .|| <= r by XCMPLX_1:87;
r < r0 by A8,XREAL_1:216;
hence ||. h/.x1 - h/.x0 .|| < r0 by A26,XXREAL_0:2;
end;
hence thesis by A7,A6,NFCONT_3:8;
end;
theorem
for n be non zero Element of NAT,
h be PartFunc of REAL, REAL-NS n holds
h is continuous iff
for i be Element of NAT st i in Seg n
holds Proj(i,n)*h is continuous
proof
let n be non zero Element of NAT,
h be PartFunc of REAL, REAL-NS n;
hereby assume
A1: h is continuous;
thus for i be Element of NAT st i in Seg n
holds Proj(i,n)*h is continuous
proof
let i be Element of NAT;
assume
A2: i in Seg n;
A3: dom Proj(i,n) = the carrier of REAL-NS n by FUNCT_2:def 1;
rng h c= the carrier of REAL-NS n; then
A4: dom (Proj(i,n)*h) = dom h by A3,RELAT_1:27;
for x0 st x0 in dom (Proj(i,n)*h)
holds Proj(i,n)*h is_continuous_in x0 by A2,Th46,A1,A4;
hence Proj(i,n)*h is continuous;
end;
end;
assume
A5: for i be Element of NAT st i in Seg n holds Proj(i,n)*h is continuous;
let x0;
assume A6: x0 in dom h;
now let i be Element of NAT;
assume A7: i in Seg n;
A8: dom (Proj(i,n)) = the carrier of REAL-NS n by FUNCT_2:def 1;
rng h c= the carrier of REAL-NS n; then
A9: dom (Proj(i,n)*h) = dom h by A8,RELAT_1:27;
Proj(i,n)*h is continuous by A5,A7;
hence Proj(i,n)*h is_continuous_in x0 by A6,A9;
end;
hence h is_continuous_in x0 by Th46;
end;