:: The Continuous Functions on Normed Linear Spaces
:: by Takaya Nishiyama, Keiji Ohkubo and Yasunari Shidama
::
:: Received April 6, 2004
:: Copyright (c) 2004-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, REAL_1, NORMSP_1, PARTFUN1, NAT_1, PRE_TOPC,
XBOOLE_0, ALGSTR_0, ARYTM_1, ARYTM_3, FUNCT_1, RELAT_1, STRUCT_0,
RCOMP_1, CARD_1, TARSKI, XXREAL_0, SUPINF_2, VALUED_0, SEQ_2, ORDINAL2,
FCONT_1, FUNCT_2, COMPLEX1, VALUED_1, CFCONT_1, SEQ_1, SEQ_4, NFCONT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
PARTFUN2, FUNCT_2, PRE_TOPC, VALUED_0, STRUCT_0, ALGSTR_0, ORDINAL1,
NUMBERS, XCMPLX_0, COMPLEX1, REAL_1, XREAL_0, RLVECT_1, SEQ_1, SEQ_2,
SEQ_4, RCOMP_1, VFUNCT_1, NORMSP_0, NORMSP_1, XXREAL_0;
constructors REAL_1, COMPLEX1, SEQ_2, SEQ_4, RCOMP_1, PARTFUN2, VFUNCT_1,
RELSET_1, COMSEQ_2;
registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, NAT_1, STRUCT_0,
RLVECT_1, VALUED_0, XREAL_0, VFUNCT_1, FUNCT_2;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions TARSKI;
equalities RLVECT_1, RELAT_1;
expansions TARSKI;
theorems TARSKI, XBOOLE_0, XBOOLE_1, RLVECT_1, XCMPLX_0, XCMPLX_1, ZFMISC_1,
RCOMP_1, SEQ_2, RELAT_1, FUNCT_1, VFUNCT_1, LOPBAN_1, FUNCT_2, SEQ_4,
NORMSP_1, PARTFUN1, PARTFUN2, XREAL_1, COMPLEX1, XXREAL_0, BHSP_1,
VALUED_0, NORMSP_0, ORDINAL1;
schemes FUNCT_2;
begin :: Continuous Functions on Normed Linear Spaces
reserve n,m for Nat;
reserve x,X,X1 for set;
reserve s,g,r,p for Real;
reserve S,T for RealNormSpace;
reserve f,f1,f2 for PartFunc of S,T;
reserve s1,s2 for sequence of S;
reserve x0,x1,x2 for Point of S;
reserve Y for Subset of S;
theorem
for S being non empty addLoopStr for seq1,seq2 be sequence of S holds
seq1 - seq2 = seq1 +- seq2
proof
let S be non empty addLoopStr;
let seq1, seq2 be sequence of S;
for n being Element of NAT holds (seq1 - seq2).n = (seq1 +- seq2).n
proof
let n be Element of NAT;
thus (seq1 - seq2).n = seq1.n - seq2.n by NORMSP_1:def 3
.= seq1.n + (-seq2).n by BHSP_1:44
.= (seq1+-seq2).n by NORMSP_1:def 2;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th2:
for seq be sequence of S holds -seq=(-1)*seq
proof
let seq be sequence of S;
now
let n be Element of NAT;
thus ((-1)*seq).n =(-1)*seq.n by NORMSP_1:def 5
.=-seq.n by RLVECT_1:16
.=(-seq).n by BHSP_1:44;
end;
hence thesis by FUNCT_2:63;
end;
definition
let S, x0;
mode Neighbourhood of x0 -> Subset of S means
:Def1:
ex g be Real
st 00;
set N= {y where y is Point of S : ||.y-x0 .|| < g};
N c= the carrier of S
proof
let x be object;
assume x in {y where y is Point of S : ||.y-x0 .|| < g};
then ex y be Point of S st x=y & ||.y-x0 .|| < g;
hence thesis;
end;
hence thesis by A1,Def1;
end;
theorem Th4:
for N being Neighbourhood of x0 holds x0 in N
proof
let N be Neighbourhood of x0;
consider g be Real such that
A1: 0= r by A3;
take p;
thus thesis by A5;
end;
consider s1 being sequence of S such that
A6: for n being Element of NAT holds P[n,s1.n] from FUNCT_2:sch 3(A4);
reconsider s1 as sequence of S;
A7: rng s1 c= dom f
proof
A8: dom s1= NAT by FUNCT_2:def 1;
let v be object;
assume v in rng s1;
then ex n be object st n in NAT & v=s1.n by A8,FUNCT_1:def 3;
hence thesis by A6;
end;
A9: now
let n;
A10: n in NAT by ORDINAL1:def 12;
|.f/.(s1.n)-f/.x0 .|>=r by A6,A10;
hence |. (f/*s1).n-f/.x0 .| >= r by A7,FUNCT_2:109,A10;
end;
A11: now
let s be Real;
consider n being Nat such that
A12: s"0;
set y=x1-x0;
consider s such that
A9: 0~~0 by A9;
let x2 such that
x2 in the carrier of S and
A11: ||. x2-x1 .||~~~~{} & (dom f
) is compact & f is_continuous_on (dom f) ex x1,x2 st x1 in dom f & x2 in dom f
& f/.x1 = upper_bound (rng f) & f/.x2 = lower_bound (rng f)
proof
let f be PartFunc of the carrier of S,REAL;
assume dom f <> {} & dom f is compact & f is_continuous_on (dom f);
then
A1: rng f <> {} & rng f is compact by Th31,RELAT_1:42;
then consider x being Element of S such that
A2: x in dom f & upper_bound (rng f) = f.x by PARTFUN1:3,RCOMP_1:14;
take x;
consider y being Element of S such that
A3: y in dom f & lower_bound (rng f ) = f.y by A1,PARTFUN1:3,RCOMP_1:14;
take y;
thus thesis by A2,A3,PARTFUN1:def 6;
end;
theorem Th34:
for f st dom f<>{} & (dom f) is compact & f is_continuous_on (
dom f) ex x1,x2 st x1 in dom f & x2 in dom f & ||.f.||/.x1 = upper_bound (rng
||.f.||) & ||.f.||/.x2 = lower_bound (rng ||.f.||)
proof
let f such that
A1: dom f <> {} and
A2: dom f is compact and
A3: f is_continuous_on (dom f);
A4: dom f = dom ||.f.|| by NORMSP_0:def 3;
dom ||.f.|| is compact by A2,NORMSP_0:def 3;
then
A5: rng ||.f.|| is compact by A3,A4,Th28,Th31;
A6: rng ||.f.|| <> {} by A1,A4,RELAT_1:42;
then consider x being Element of S such that
A7: x in dom ||.f.|| & upper_bound (rng ||.f.||) = ||.f.||.x by A5,PARTFUN1:3
,RCOMP_1:14;
consider y being Element of S such that
A8: y in dom ||.f.|| & lower_bound (rng ||.f.||) = ||.f.||.y by A6,A5,
PARTFUN1:3,RCOMP_1:14;
take x;
take y;
thus thesis by A7,A8,NORMSP_0:def 3,PARTFUN1:def 6;
end;
theorem Th35:
(||.f.||)|X = ||.(f|X).||
proof
A1: dom ((||.f.||)|X) = dom (||.f.||) /\ X by RELAT_1:61
.= dom f /\ X by NORMSP_0:def 3
.= dom (f|X) by RELAT_1:61
.= dom ( ||.(f|X).||) by NORMSP_0:def 3;
now
let c be Point of S;
assume
A2: c in dom ((||.f.||)|X);
then
A3: c in dom (f|X) by A1,NORMSP_0:def 3;
c in dom (||.f.||) /\ X by A2,RELAT_1:61;
then
A4: c in dom (||.f.||) by XBOOLE_0:def 4;
thus ((||.f.||)|X).c = (||.f.||).c by A2,FUNCT_1:47
.= ||.f/.c.|| by A4,NORMSP_0:def 3
.= ||.(f|X)/.c.|| by A3,PARTFUN2:15
.= ||.(f|X).||.c by A1,A2,NORMSP_0:def 3;
end;
hence thesis by A1,PARTFUN1:5;
end;
theorem
for f,Y st Y<>{} & Y c= dom f & Y is compact & f is_continuous_on Y ex
x1,x2 st x1 in Y & x2 in Y & ||.f.||/.x1 = upper_bound (||.f.||.:Y) & ||.f.||/.
x2 = lower_bound (||.f.||.:Y)
proof
let f,Y such that
A1: Y <> {} and
A2: Y c= dom f and
A3: Y is compact and
A4: f is_continuous_on Y;
A5: dom (f|Y) = dom f /\ Y by RELAT_1:61
.= Y by A2,XBOOLE_1:28;
f|Y is_continuous_on Y
proof
thus Y c= dom (f|Y) by A5;
let r be Point of S;
assume r in Y;
then f|Y is_continuous_in r by A4;
hence thesis by RELAT_1:72;
end;
then consider x1,x2 such that
A6: x1 in dom (f|Y) and
A7: x2 in dom (f|Y) and
A8: ||.(f|Y).||/.x1 = upper_bound (rng ||.(f|Y).||) & ||.(f|Y).||/.x2 =
lower_bound (rng ||.(f|Y).||) by A1,A3,A5,Th34;
A9: dom f = dom ||.f.|| by NORMSP_0:def 3;
take x1,x2;
thus x1 in Y & x2 in Y by A5,A6,A7;
A10: ||.f.||.:Y =rng ( ||.f.|| | Y) by RELAT_1:115
.=rng( ||.(f|Y).|| ) by Th35;
A11: x2 in dom ||.(f|Y).|| by A7,NORMSP_0:def 3;
then
A12: ||.(f|Y).||/.x2 =||.(f|Y).||.x2 by PARTFUN1:def 6
.=||. (f|Y)/.x2.|| by A11,NORMSP_0:def 3
.=||. f/.x2.|| by A7,PARTFUN2:15
.=||. f.||.x2 by A2,A5,A7,A9,NORMSP_0:def 3
.=||. f.||/.x2 by A2,A5,A7,A9,PARTFUN1:def 6;
A13: x1 in dom ||.(f|Y).|| by A6,NORMSP_0:def 3;
then ||.(f|Y).||/.x1 =||.(f|Y).||.x1 by PARTFUN1:def 6
.=||. (f|Y)/.x1.|| by A13,NORMSP_0:def 3
.=||. f/.x1.|| by A6,PARTFUN2:15
.=||. f.||.x1 by A2,A5,A6,A9,NORMSP_0:def 3
.=||. f.||/.x1 by A2,A5,A6,A9,PARTFUN1:def 6;
hence thesis by A8,A12,A10;
end;
theorem
for f be PartFunc of the carrier of S,REAL for Y st Y<>{} & Y c= dom f
& Y is compact & f is_continuous_on Y ex x1,x2 st x1 in Y & x2 in Y & f/.x1 =
upper_bound (f.:Y) & f/.x2 = lower_bound (f.:Y)
proof
let f be PartFunc of the carrier of S,REAL;
let Y such that
A1: Y <> {} and
A2: Y c= dom f and
A3: Y is compact and
A4: f is_continuous_on Y;
A5: dom (f|Y) = dom f /\ Y by RELAT_1:61
.= Y by A2,XBOOLE_1:28;
f|Y is_continuous_on Y
proof
thus Y c= dom (f|Y) by A5;
let r be Point of S;
assume r in Y;
then f|Y is_continuous_in r by A4;
hence thesis by RELAT_1:72;
end;
then consider x1,x2 such that
A6: x1 in dom (f|Y) & x2 in dom (f|Y) and
A7: (f|Y)/.x1 = upper_bound (rng (f|Y)) & (f|Y)/.x2 = lower_bound (rng
(f|Y)) by A1,A3,A5,Th33;
take x1,x2;
thus x1 in Y & x2 in Y by A5,A6;
(f|Y)/.x1 =f/.x1 & (f|Y)/.x2 =f/.x2 by A6,PARTFUN2:15;
hence thesis by A7,RELAT_1:115;
end;
definition
let S,T;
let X,f;
pred f is_Lipschitzian_on X means
X c= dom f & ex r st 00;
take g = |.p.| *s;
0<|.p.| by A9,COMPLEX1:47;
then 0*s<|.p.|*s by A2,XREAL_1:68;
hence 00;
let x1,x2;
assume that
A1: x1 in Y and
A2: x2 in Y;
||. (id Y)/.x1-(id Y)/.x2 .|| = ||. x1-(id Y)/.x2 .|| by A1,PARTFUN2:6
.= r*||. x1-x2 .|| by A2,PARTFUN2:6;
hence thesis;
end;
theorem Th45:
f is_Lipschitzian_on X implies f is_continuous_on X
proof
assume
A1: f is_Lipschitzian_on X;
then consider r such that
A2: 0~~