:: Continuous Functions on Real and Complex Normed Linear Spaces
:: by Noboru Endou
::
:: Received August 20, 2004
:: Copyright (c) 2004-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, REAL_1, XCMPLX_0, CLVECT_1, NORMSP_1, NAT_1,
ARYTM_1, ARYTM_3, COMPLEX1, RELAT_1, FUNCT_1, PARTFUN1, STRUCT_0,
PRE_TOPC, RCOMP_1, CARD_1, TARSKI, XXREAL_0, SUPINF_2, VALUED_0, SEQ_2,
ORDINAL2, FCONT_1, FUNCT_2, XBOOLE_0, VALUED_1, CFCONT_1, COMSEQ_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, XREAL_0, ORDINAL1, NUMBERS, XCMPLX_0,
COMPLEX1, REAL_1, NAT_1, RLVECT_1, SEQ_1, SEQ_2, VALUED_0, SEQ_4,
VFUNCT_1, COMSEQ_1, CFCONT_1, RCOMP_1, COMSEQ_2, STRUCT_0, VFUNCT_2,
CLVECT_1, NFCONT_1, XXREAL_0, NORMSP_0, NORMSP_1;
constructors REAL_1, SEQ_4, RCOMP_1, PARTFUN2, COMSEQ_2, COMSEQ_3, CFCONT_1,
NFCONT_1, VFUNCT_2, SEQ_2, RELSET_1;
registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, NAT_1, STRUCT_0,
VALUED_0, XREAL_0, VFUNCT_1, FUNCT_2, XCMPLX_0;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions TARSKI, NFCONT_1;
equalities RELAT_1;
expansions TARSKI, NFCONT_1;
theorems TARSKI, ABSVALUE, 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, CLVECT_1, COMSEQ_2, VFUNCT_2,
NFCONT_1, CLOPBAN1, CFCONT_1, COMPLEX1, XREAL_1, XXREAL_0, BHSP_1,
VALUED_0, NORMSP_0, ORDINAL1;
schemes FUNCT_2;
begin :: Continuous Function on Normed Complex Linear Spaces
reserve n,m for Element of NAT;
reserve r,s for Real;
reserve z for Complex;
reserve CNS,CNS1,CNS2 for ComplexNormSpace;
reserve RNS for RealNormSpace;
theorem Th1:
for seq be sequence of CNS holds -seq=(-1r)*seq
proof
let seq be sequence of CNS;
now
let n;
thus ((-1r)*seq).n =(-1r)*seq.n by CLVECT_1:def 14
.=-seq.n by CLVECT_1:3
.=(-seq).n by BHSP_1:44;
end;
hence thesis by FUNCT_2:63;
end;
definition
let CNS;
let x0 be Point of CNS;
mode Neighbourhood of x0 -> Subset of CNS means
:Def1:
ex g be Real st 00;
set N= {y where y is Point of CNS : ||.y-x0 .|| < g};
N c= the carrier of CNS
proof
let x be object;
assume x in {y where y is Point of CNS : ||.y-x0 .|| < g};
then ex y be Point of CNS st x=y & ||.y-x0 .|| < g;
hence thesis;
end;
hence thesis by A1,Def1;
end;
theorem Th3:
for x0 be Point of CNS for N being Neighbourhood of x0 holds x0 in N
proof
let x0 be Point of CNS;
let N be Neighbourhood of x0;
consider g be Real such that
A1: 00;
set y=x1-x0;
consider s such that
A9: 0~~0 by A9;
let x2 be Point of CNS1 such that
x2 in the carrier of CNS1 and
A11: ||. x2-x1 .||~~~~0;
set y=x1-x0;
consider s such that
A9: 0~~~~0 by A9;
let x2 be Point of CNS such that
x2 in the carrier of CNS and
A11: ||. x2-x1 .||~~~~0;
set y=x1-x0;
consider s such that
A9: 0~~~~0 by A9;
let x2 be Point of RNS such that
x2 in the carrier of RNS and
A11: ||. x2-x1 .||~~~~{} & (
dom f) is compact & f is_continuous_on (dom f) holds ex x1,x2 be Point of CNS
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 CNS,REAL;
assume dom f <> {} & dom f is compact & f is_continuous_on (dom f);
then
A1: rng f <> {} & rng f is compact by Th81,RELAT_1:42;
then consider x being Element of CNS 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 CNS 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 Th87:
for f be PartFunc of CNS1,CNS2 st dom f<>{} & (dom f) is
compact & f is_continuous_on (dom f) holds ex x1,x2 be Point of CNS1 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 CNS1,CNS2 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,Th71,Th81;
A6: rng ||.f.|| <> {} by A1,A4,RELAT_1:42;
then consider x being Element of CNS1 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 CNS1 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 Th88:
for f be PartFunc of CNS,RNS st dom f<>{} & (dom f) is compact
& f is_continuous_on (dom f) holds ex x1,x2 be Point of CNS 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 CNS,RNS 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,Th72,Th81;
A6: rng ||.f.|| <> {} by A1,A4,RELAT_1:42;
then consider x being Element of CNS 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 CNS 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 Th89:
for f be PartFunc of RNS,CNS st dom f<>{} & (dom f) is compact
& f is_continuous_on (dom f) holds ex x1,x2 be Point of RNS 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 RNS,CNS 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,Th73,NFCONT_1:31;
A6: rng ||.f.|| <> {} by A1,A4,RELAT_1:42;
then consider x being Element of RNS 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 RNS 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 Th90:
for f be PartFunc of CNS1,CNS2 holds (||.f.||)|X = ||.(f|X).||
proof
let f be PartFunc of CNS1,CNS2;
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 CNS1;
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 Th91:
for f be PartFunc of CNS,RNS holds (||.f.||)|X = ||.(f|X).||
proof
let f be PartFunc of CNS,RNS;
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 CNS;
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 Th92:
for f be PartFunc of RNS,CNS holds (||.f.||)|X = ||.(f|X).||
proof
let f be PartFunc of RNS,CNS;
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 RNS;
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 be PartFunc of CNS1,CNS2, Y be Subset of CNS1 st Y<>{} & Y c=
dom f & Y is compact & f is_continuous_on Y holds ex x1,x2 be Point of CNS1 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 CNS1,CNS2;
let Y be Subset of CNS1 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 CNS1;
assume r in Y;
then f|Y is_continuous_in r by A4;
hence thesis by RELAT_1:72;
end;
then consider x1,x2 be Point of CNS1 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,Th87;
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 Th90;
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 CNS,RNS,Y be Subset of CNS st Y<>{} & Y c= dom f
& Y is compact & f is_continuous_on Y holds ex x1,x2 be Point of CNS 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 CNS,RNS;
let Y be Subset of CNS 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 CNS;
assume r in Y;
then f|Y is_continuous_in r by A4;
hence thesis by RELAT_1:72;
end;
then consider x1,x2 be Point of CNS 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,Th88;
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 Th91;
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 RNS,CNS,Y be Subset of RNS st Y<>{} & Y c= dom f
& Y is compact & f is_continuous_on Y holds ex x1,x2 be Point of RNS 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 RNS,CNS;
let Y be Subset of RNS 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 RNS;
assume r in Y;
then f|Y is_continuous_in r by A4;
hence thesis by RELAT_1:72;
end;
then consider x1,x2 be Point of RNS 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,Th89;
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 Th92;
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 CNS,REAL, Y be Subset of CNS st Y
<>{} & Y c= dom f & Y is compact & f is_continuous_on Y holds ex x1,x2 be Point
of CNS 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 CNS,REAL;
let Y be Subset of CNS 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 CNS;
assume r in Y;
then f|Y is_continuous_in r by A4;
hence thesis by RELAT_1:72;
end;
then consider x1,x2 be Point of CNS 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,Th86;
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 CNS1,CNS2 be ComplexNormSpace;
let X be set;
let f be PartFunc of CNS1,CNS2;
pred f is_Lipschitzian_on X means
X c= dom f & ex r st 0 < r & for
x1,x2 be Point of CNS1 st x1 in X & x2 in X holds ||.f/.x1-f/.x2.||<=r*||.x1-x2
.||;
end;
definition
let CNS be ComplexNormSpace;
let RNS be RealNormSpace;
let X be set;
let f be PartFunc of CNS,RNS;
pred f is_Lipschitzian_on X means
X c= dom f & ex r st 0 < r & for
x1,x2 be Point of CNS st x1 in X & x2 in X holds ||.f/.x1-f/.x2.||<=r*||.x1-x2
.||;
end;
definition
let RNS be RealNormSpace;
let CNS be ComplexNormSpace;
let X be set;
let f be PartFunc of RNS,CNS;
pred f is_Lipschitzian_on X means
X c= dom f & ex r st 0 < r & for
x1,x2 be Point of RNS st x1 in X & x2 in X holds ||.f/.x1-f/.x2.||<=r*||.x1-x2
.||;
end;
definition
let CNS be ComplexNormSpace;
let X be set;
let f be PartFunc of the carrier of CNS,COMPLEX;
pred f is_Lipschitzian_on X means
X c= dom f & ex r st 00;
reconsider g = |.z.| *s as Real;
take g;
0<|.z.| by A9,COMPLEX1:47;
then 0*s<|.z.|*s by A2,XREAL_1:68;
hence 00;
reconsider g = |.r.| *s as Real;
take g;
0<|.r.| by A9,COMPLEX1:47;
then 0*s<|.r.|*s by A2,XREAL_1:68;
hence 00;
reconsider g = |.z.| *s as Real;
take g;
0<|.z.| by A9,COMPLEX1:47;
then 0*s<|.z.|*s by A2,XREAL_1:68;
hence 00;
let x1,x2 be Point of CNS;
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 Th116:
for f be PartFunc of CNS1,CNS2 st f is_Lipschitzian_on X holds
f is_continuous_on X
proof
let f be PartFunc of CNS1,CNS2;
assume
A1: f is_Lipschitzian_on X;
then consider r be Real such that
A2: 0 < r and
A3: for x1,x2 be Point of CNS1 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 be Point of CNS1 such that
A6: x0 in X;
now
let g be Real such that
A7: 0= - (||.x1 - x2.||) by CLVECT_1:109,XREAL_1:24;
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 A2,ABSVALUE:5;
end;
then f is_Lipschitzian_on dom f;
hence thesis by Th120;
end;
theorem
for f be PartFunc of the carrier of CNS,REAL st X c= dom f & (for x0
be Point of CNS st x0 in X holds f/.x0 = ||. x0.||) holds f is_continuous_on X
proof
let f be PartFunc of the carrier of CNS,REAL;
assume that
A1: X c= dom f and
A2: for x0 be Point of CNS 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 be Point of CNS;
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,Th132;
hence thesis by Th54;
end;
~~