:: More on Continuous Functions on Normed Linear Spaces
:: by Hiroyuki Okazaki , Noboru Endou and Yasunari Shidama
::
:: Received August 17, 2010
:: Copyright (c) 2010-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, XXREAL_1, VALUED_1, ZFMISC_1,
VALUED_0, FCONT_1, NORMSP_1, STRUCT_0, SUPINF_2, PRE_TOPC;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1,
PARTFUN1, FUNCT_2, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, NAT_1,
VALUED_0, COMPLEX1, ZFMISC_1, SEQ_1, SEQ_2, RCOMP_1, FCONT_1, STRUCT_0,
PRE_TOPC, RLVECT_1, VFUNCT_1, NORMSP_0, NORMSP_1, NFCONT_1;
constructors REAL_1, COMPLEX1, MEMBERED, SEQ_2, RCOMP_1, RELSET_1, FCONT_1,
NFCONT_1, VFUNCT_1, COMSEQ_2, NUMBERS;
registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED,
VALUED_0, FUNCT_2, RELAT_1, FUNCT_1, STRUCT_0, VFUNCT_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin :: Preliminaries
reserve n,m,k for Nat;
reserve x,X,X1 for set;
reserve r,p for Real;
reserve s,g,x0,x1,x2 for Real;
reserve S,T for RealNormSpace;
reserve f,f1,f2 for PartFunc of REAL,the carrier of S;
reserve s1,s2 for Real_Sequence;
reserve Y for Subset of REAL;
theorem :: NFCONT_3:1
for seq be Real_Sequence, h be PartFunc of REAL, the carrier of S
st rng seq c= dom h holds seq.n in dom h;
theorem :: NFCONT_3:2
for h1,h2 be PartFunc of REAL,the carrier of S
for seq be Real_Sequence
st rng seq c= dom h1 /\ dom h2
holds (h1+h2)/*seq = h1/*seq + h2/*seq & (h1-h2)/*seq = h1/*seq - h2/*seq;
theorem :: NFCONT_3:3
for h be sequence of S,r be Real holds r(#)h = r*h;
theorem :: NFCONT_3:4
for h be PartFunc of REAL,the carrier of S,
seq be Real_Sequence, r be Real
st rng seq c= dom h holds (r(#)h)/*seq = r*(h/*seq);
theorem :: NFCONT_3:5
for h be PartFunc of REAL,the carrier of S,
seq be Real_Sequence
st rng seq c= dom h
holds ||.h/*seq .|| = ||.h.||/*seq
& -(h/*seq) = (-h)/*seq;
begin :: Continuous Real Functions into Normed Linear Spaces
definition
let S,f,x0;
pred f is_continuous_in x0 means
:: NFCONT_3:def 1
x0 in dom f
& for s1 st rng s1 c= dom f & s1 is convergent & lim s1 = x0
holds f/*s1 is convergent & f/.x0 = lim (f/*s1);
end;
theorem :: NFCONT_3:6
x0 in X & f is_continuous_in x0 implies f|X is_continuous_in x0;
theorem :: NFCONT_3:7
f is_continuous_in x0 iff
x0 in dom f
& for s1 st rng s1 c= dom f & s1 is convergent
& lim s1 = x0 & (for n holds s1.n<>x0)
holds f/*s1 is convergent & f/.x0 = lim(f/*s1);
theorem :: NFCONT_3:8
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;
theorem :: NFCONT_3:9
for S,f,x0 holds f is_continuous_in x0 iff
x0 in dom f
& for N1 being Neighbourhood of f/.x0
ex N being Neighbourhood of x0
st for x1 st x1 in dom f & x1 in N holds f/.x1 in N1;
theorem :: NFCONT_3:10
for S,f,x0 holds
f is_continuous_in x0
iff x0 in dom f
& for N1 being Neighbourhood of f/.x0
ex N being Neighbourhood of x0 st f.:N c= N1;
theorem :: NFCONT_3:11
(ex N be Neighbourhood of x0 st dom f /\ N = {x0})
implies f is_continuous_in x0;
theorem :: NFCONT_3:12
x0 in dom f1 /\ dom f2 & f1 is_continuous_in x0 & f2 is_continuous_in x0
implies f1+f2 is_continuous_in x0 & f1-f2 is_continuous_in x0;
theorem :: NFCONT_3:13
f is_continuous_in x0 implies r(#)f is_continuous_in x0;
theorem :: NFCONT_3:14
x0 in dom f & f is_continuous_in x0
implies ||.f.|| is_continuous_in x0 & -f is_continuous_in x0;
theorem :: NFCONT_3:15
for f1 be PartFunc of REAL,the carrier of S,
f2 be PartFunc of the carrier of S,the carrier of T
st x0 in dom (f2*f1) & f1 is_continuous_in x0
& f2 is_continuous_in f1/.x0
holds f2*f1 is_continuous_in x0;
definition let S,f;
attr f is continuous means
:: NFCONT_3:def 2
for x0 st x0 in dom f holds f is_continuous_in x0;
end;
theorem :: NFCONT_3:16
for X,f st X c= dom f holds f|X is continuous
iff for s1 st rng s1 c= X & s1 is convergent & lim s1 in X
holds f/*s1 is convergent & f/.(lim s1) = lim (f/*s1);
theorem :: NFCONT_3:17
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);
registration let S;
cluster constant -> continuous for PartFunc of REAL,the carrier of S;
end;
registration let S;
cluster continuous for PartFunc of REAL,the carrier of S;
end;
registration let S;
let f be continuous PartFunc of REAL,the carrier of S, X be set;
cluster f|X -> continuous for PartFunc of REAL,the carrier of S;
end;
theorem :: NFCONT_3:18
f|X is continuous & X1 c= X implies f|X1 is continuous;
registration let S;
cluster empty -> continuous for PartFunc of REAL,the carrier of S;
end;
registration let S,f;
let X be trivial set;
cluster f|X -> continuous for PartFunc of REAL,the carrier of S;
end;
registration
let S;
let f1,f2 be continuous PartFunc of REAL,the carrier of S;
cluster f1+f2 -> continuous for PartFunc of REAL,the carrier of S;
cluster f1-f2 -> continuous for PartFunc of REAL,the carrier of S;
end;
theorem :: NFCONT_3:19
for X,f1,f2 st X c= dom f1 /\ dom f2 & f1|X is continuous & f2|X is continuous
holds (f1+f2)|X is continuous & (f1-f2)|X is continuous;
theorem :: NFCONT_3:20
for X,X1,f1,f2 st X c= dom f1 & X1 c= dom f2
& f1|X is continuous & f2|X1 is continuous
holds (f1+f2)|(X /\ X1) is continuous & (f1-f2)|(X /\ X1) is continuous;
registration
let S;
let f be continuous PartFunc of REAL,the carrier of S;
let r;
cluster r(#)f -> continuous for PartFunc of REAL,the carrier of S;
end;
theorem :: NFCONT_3:21
X c= dom f & f|X is continuous implies (r(#)f)|X is continuous;
theorem :: NFCONT_3:22
X c= dom f & f|X is continuous
implies (||.f.||)|X is continuous & (-f)|X is continuous;
theorem :: NFCONT_3:23
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;
theorem :: NFCONT_3:24
dom f is compact & f|(dom f) is continuous implies rng f is compact;
theorem :: NFCONT_3:25
Y c= dom f & Y is compact & f|Y is continuous implies (f.:Y) is compact;
begin :: Lipschitz continuity
definition let S,f;
attr f is Lipschitzian means
:: NFCONT_3:def 3
ex r be Real st 0 Lipschitzian for PartFunc of REAL,the carrier of S;
end;
registration let S;
cluster empty for PartFunc of REAL,the carrier of S;
end;
registration
let S;
let f be Lipschitzian PartFunc of REAL,the carrier of S, X be set;
cluster f|X -> Lipschitzian for PartFunc of REAL,the carrier of S;
end;
theorem :: NFCONT_3:27
f|X is Lipschitzian & X1 c= X implies f|X1 is Lipschitzian;
registration
let S;
let f1,f2 be Lipschitzian PartFunc of REAL,the carrier of S;
cluster f1+f2 -> Lipschitzian for PartFunc of REAL,the carrier of S;
cluster f1-f2 -> Lipschitzian for PartFunc of REAL,the carrier of S;
end;
theorem :: NFCONT_3:28
f1|X is Lipschitzian & f2|X1 is Lipschitzian
implies (f1+f2)|(X /\ X1) is Lipschitzian;
theorem :: NFCONT_3:29
f1|X is Lipschitzian & f2|X1 is Lipschitzian
implies (f1-f2)|(X /\ X1) is Lipschitzian;
registration
let S;
let f be Lipschitzian PartFunc of REAL, the carrier of S;
let p;
cluster p(#)f -> Lipschitzian for PartFunc of REAL, the carrier of S;
end;
theorem :: NFCONT_3:30
f|X is Lipschitzian & X c= dom f implies (p(#)f) | X is Lipschitzian;
registration let S;
let f be Lipschitzian PartFunc of REAL, the carrier of S;
cluster ||. f .|| -> Lipschitzian for PartFunc of REAL,REAL;
end;
theorem :: NFCONT_3:31
f|X is Lipschitzian
implies -(f|X) is Lipschitzian & (-f)|X is Lipschitzian
& (||.f.||)|X is Lipschitzian;
registration let S;
cluster constant -> Lipschitzian for PartFunc of REAL, the carrier of S;
end;
registration let S;
cluster Lipschitzian -> continuous for PartFunc of REAL, the carrier of S;
end;
theorem :: NFCONT_3:32
(ex r be Point of S st rng f = {r}) implies f is continuous;
theorem :: NFCONT_3:33
for r, p be Point of S st (for x0 st x0 in X holds f/.x0 = x0*r+p)
holds f|X is continuous;