:: More on Continuous Functions on Normed Linear Spaces
:: by Hiroyuki Okazaki , Noboru Endou and Yasunari Shidama
::
:: Received August 17, 2010
:: Copyright (c) 2010-2012 Association of Mizar Users


begin

theorem Th1: :: NFCONT_3:1
for n being Element of NAT
for S being RealNormSpace
for seq being Real_Sequence
for h being PartFunc of REAL, the carrier of S st rng seq c= dom h holds
seq . n in dom h
proofend;

theorem Th2: :: NFCONT_3:2
for S being RealNormSpace
for h1, h2 being PartFunc of REAL, the carrier of S
for seq being 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) )
proofend;

theorem :: NFCONT_3:3
for S being RealNormSpace
for h being sequence of S
for r being Real holds r (#) h = r * h
proofend;

theorem Th4: :: NFCONT_3:4
for S being RealNormSpace
for h being PartFunc of REAL, the carrier of S
for seq being Real_Sequence
for r being Real st rng seq c= dom h holds
(r (#) h) /* seq = r * (h /* seq)
proofend;

theorem Th5: :: NFCONT_3:5
for S being RealNormSpace
for h being PartFunc of REAL, the carrier of S
for seq being Real_Sequence st rng seq c= dom h holds
( ||.(h /* seq).|| = ||.h.|| /* seq & - (h /* seq) = (- h) /* seq )
proofend;

begin

definition
let S be RealNormSpace;
let f be PartFunc of REAL, the carrier of S;
let x0 be real number ;
predf is_continuous_in x0 means :Def1: :: NFCONT_3:def 1
( x0 in dom f & ( for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) );
end;

:: deftheorem Def1 defines is_continuous_in NFCONT_3:def_1_:_
 for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S
for x0 being real number holds
( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) );

theorem Th6: :: NFCONT_3:6
for X being set
for x0 being real number
for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S st x0 in X & f is_continuous_in x0 holds
f | X is_continuous_in x0
proofend;

theorem :: NFCONT_3:7
for x0 being real number
for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S holds
( f is_continuous_in x0 iff ( x0 in dom f &amp; ( for s1 being Real_Sequence st rng s1 c= dom f &amp; s1 is convergent &amp; lim s1 = x0 &amp; ( for n being Element of NAT holds s1 . n <> x0 ) holds
( f /* s1 is convergent &amp; f /. x0 = lim (f /* s1) ) ) ) )
proofend;

theorem Th8: :: NFCONT_3:8
for x0 being real number
for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S holds
( f is_continuous_in x0 iff ( x0 in dom f &amp; ( for r being Real st 0 < r holds
ex s being real number st
( 0 < s &amp; ( for x1 being real number st x1 in dom f &amp; abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) )
proofend;

theorem Th9: :: NFCONT_3:9
for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S
for x0 being real number holds
( f is_continuous_in x0 iff ( x0 in dom f &amp; ( for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f &amp; x1 in N holds
f /. x1 in N1 ) ) )
proofend;

theorem Th10: :: NFCONT_3:10
for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S
for x0 being real number holds
( f is_continuous_in x0 iff ( x0 in dom f &amp; ( for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st f .: N c= N1 ) ) )
proofend;

theorem :: NFCONT_3:11
for x0 being real number
for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S st ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} holds
f is_continuous_in x0
proofend;

theorem :: NFCONT_3:12
for x0 being real number
for S being RealNormSpace
for f1, f2 being PartFunc of REAL, the carrier of S st x0 in (dom f1) /\ (dom f2) &amp; f1 is_continuous_in x0 &amp; f2 is_continuous_in x0 holds
( f1 + f2 is_continuous_in x0 &amp; f1 - f2 is_continuous_in x0 )
proofend;

theorem Th13: :: NFCONT_3:13
for r being Real
for x0 being real number
for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S st f is_continuous_in x0 holds
r (#) f is_continuous_in x0
proofend;

theorem :: NFCONT_3:14
for x0 being real number
for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S st x0 in dom f &amp; f is_continuous_in x0 holds
( ||.f.|| is_continuous_in x0 &amp; - f is_continuous_in x0 )
proofend;

theorem :: NFCONT_3:15
for x0 being real number
for S, T being RealNormSpace
for f1 being PartFunc of REAL, the carrier of S
for f2 being PartFunc of the carrier of S, the carrier of T st x0 in dom (f2 * f1) &amp; f1 is_continuous_in x0 &amp; f2 is_continuous_in f1 /. x0 holds
f2 * f1 is_continuous_in x0
proofend;

definition
let S be RealNormSpace;
let f be PartFunc of REAL, the carrier of S;
attrf is continuous  means :Def2: :: NFCONT_3:def 2
 for x0 being real number st x0 in dom f holds
f is_continuous_in x0;
end;

:: deftheorem Def2 defines continuous NFCONT_3:def_2_:_
 for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S holds
( f is continuous iff for x0 being real number st x0 in dom f holds
f is_continuous_in x0 );

theorem Th16: :: NFCONT_3:16
for S being RealNormSpace
for X being set
for f being PartFunc of REAL, the carrier of S st X c= dom f holds
( f | X is continuous iff for s1 being Real_Sequence st rng s1 c= X &amp; s1 is convergent &amp; lim s1 in X holds
( f /* s1 is convergent &amp; f /. (lim s1) = lim (f /* s1) ) )
proofend;

theorem Th17: :: NFCONT_3:17
for X being set
for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S st X c= dom f holds
( f | X is continuous iff for x0 being real number
for r being Real st x0 in X &amp; 0 < r holds
ex s being real number st
( 0 < s &amp; ( for x1 being real number st x1 in X &amp; abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) )
proofend;

registration
let S be RealNormSpace;
cluster Function-like constant  ->  continuous for Element of bool [:REAL, the carrier of S:];
coherence
 for b1 being PartFunc of REAL, the carrier of S st b1 is constant holds
b1 is continuous
proofend;
end;

registration
let S be RealNormSpace;
cluster Relation-like REAL -defined the carrier of S -valued Function-like continuous for Element of bool [:REAL, the carrier of S:];
existence
 ex b1 being PartFunc of REAL, the carrier of S st b1 is continuous
proofend;
end;

registration
let S be RealNormSpace;
let f be continuous PartFunc of REAL, the carrier of S;
let X be set ;
clusterf | X ->  continuous for PartFunc of REAL, the carrier of S;
coherence
 for b1 being PartFunc of REAL, the carrier of S st b1 = f | X holds
b1 is continuous
proofend;
end;

theorem Th18: :: NFCONT_3:18
for X, X1 being set
for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S st f | X is continuous &amp; X1 c= X holds
f | X1 is continuous
proofend;

registration
let S be RealNormSpace;
cluster empty Function-like  ->  continuous for Element of bool [:REAL, the carrier of S:];
coherence
 for b1 being PartFunc of REAL, the carrier of S st b1 is empty holds
b1 is continuous ;
end;

registration
let S be RealNormSpace;
let f be PartFunc of REAL, the carrier of S;
let X be trivial set ;
clusterf | X ->  continuous for PartFunc of REAL, the carrier of S;
coherence
 for b1 being PartFunc of REAL, the carrier of S st b1 = f | X holds
b1 is continuous
proofend;
end;

registration
let S be RealNormSpace;
let f1, f2 be continuous PartFunc of REAL, the carrier of S;
clusterf1 + f2 ->  continuous for PartFunc of REAL, the carrier of S;
coherence
 for b1 being PartFunc of REAL, the carrier of S st b1 = f1 + f2 holds
b1 is continuous
proofend;
clusterf1 - f2 ->  continuous for PartFunc of REAL, the carrier of S;
coherence
 for b1 being PartFunc of REAL, the carrier of S st b1 = f1 - f2 holds
b1 is continuous
proofend;
end;

theorem Th19: :: NFCONT_3:19
for S being RealNormSpace
for X being set
for f1, f2 being PartFunc of REAL, the carrier of S st X c= (dom f1) /\ (dom f2) &amp; f1 | X is continuous &amp; f2 | X is continuous holds
( (f1 + f2) | X is continuous &amp; (f1 - f2) | X is continuous )
proofend;

theorem :: NFCONT_3:20
for S being RealNormSpace
for X, X1 being set
for f1, f2 being PartFunc of REAL, the carrier of S st X c= dom f1 &amp; X1 c= dom f2 &amp; f1 | X is continuous &amp; f2 | X1 is continuous holds
( (f1 + f2) | (X /\ X1) is continuous &amp; (f1 - f2) | (X /\ X1) is continuous )
proofend;

registration
let S be RealNormSpace;
let f be continuous PartFunc of REAL, the carrier of S;
let r be Real;
clusterr (#) f ->  continuous for PartFunc of REAL, the carrier of S;
coherence
 for b1 being PartFunc of REAL, the carrier of S st b1 = r (#) f holds
b1 is continuous
proofend;
end;

theorem Th21: :: NFCONT_3:21
for X being set
for r being Real
for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S st X c= dom f &amp; f | X is continuous holds
(r (#) f) | X is continuous
proofend;

theorem :: NFCONT_3:22
for X being set
for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S st X c= dom f &amp; f | X is continuous holds
( ||.f.|| | X is continuous &amp; (- f) | X is continuous )
proofend;

theorem :: NFCONT_3:23
for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S st f is total &amp; ( for x1, x2 being real number holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) &amp; ex x0 being real number st f is_continuous_in x0 holds
f | REAL is continuous
proofend;

theorem Th24: :: NFCONT_3:24
for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S st dom f is compact &amp; f | (dom f) is continuous holds
rng f is compact
proofend;

theorem :: NFCONT_3:25
for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S
for Y being Subset of REAL st Y c= dom f &amp; Y is compact &amp; f | Y is continuous holds
f .: Y is compact
proofend;

begin

definition
let S be RealNormSpace;
let f be PartFunc of REAL, the carrier of S;
attrf is Lipschitzian  means :Def3: :: NFCONT_3:def 3
 ex r being real number st
( 0 < r &amp; ( for x1, x2 being real number st x1 in dom f &amp; x2 in dom f holds
||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) ) );
end;

:: deftheorem Def3 defines Lipschitzian NFCONT_3:def_3_:_
 for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S holds
( f is Lipschitzian iff ex r being real number st
( 0 < r &amp; ( for x1, x2 being real number st x1 in dom f &amp; x2 in dom f holds
||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) ) ) );

theorem Th26: :: NFCONT_3:26
for X being set
for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S holds
( f | X is Lipschitzian iff ex r being real number st
( 0 < r &amp; ( for x1, x2 being real number st x1 in dom (f | X) &amp; x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) ) ) )
proofend;

registration
let S be RealNormSpace;
cluster empty Function-like  ->  Lipschitzian for Element of bool [:REAL, the carrier of S:];
coherence
 for b1 being PartFunc of REAL, the carrier of S st b1 is empty holds
b1 is Lipschitzian
proofend;
end;

registration
let S be RealNormSpace;
cluster empty Relation-like REAL -defined the carrier of S -valued Function-like for Element of bool [:REAL, the carrier of S:];
existence
 ex b1 being PartFunc of REAL, the carrier of S st b1 is empty
proofend;
end;

registration
let S be RealNormSpace;
let f be Lipschitzian PartFunc of REAL, the carrier of S;
let X be set ;
clusterf | X ->  Lipschitzian for PartFunc of REAL, the carrier of S;
coherence
 for b1 being PartFunc of REAL, the carrier of S st b1 = f | X holds
b1 is Lipschitzian
proofend;
end;

theorem :: NFCONT_3:27
for X, X1 being set
for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S st f | X is Lipschitzian &amp; X1 c= X holds
f | X1 is Lipschitzian
proofend;

registration
let S be RealNormSpace;
let f1, f2 be Lipschitzian PartFunc of REAL, the carrier of S;
clusterf1 + f2 ->  Lipschitzian for PartFunc of REAL, the carrier of S;
coherence
 for b1 being PartFunc of REAL, the carrier of S st b1 = f1 + f2 holds
b1 is Lipschitzian
proofend;
clusterf1 - f2 ->  Lipschitzian for PartFunc of REAL, the carrier of S;
coherence
 for b1 being PartFunc of REAL, the carrier of S st b1 = f1 - f2 holds
b1 is Lipschitzian
proofend;
end;

theorem :: NFCONT_3:28
for X, X1 being set
for S being RealNormSpace
for f1, f2 being PartFunc of REAL, the carrier of S st f1 | X is Lipschitzian &amp; f2 | X1 is Lipschitzian holds
(f1 + f2) | (X /\ X1) is Lipschitzian
proofend;

theorem :: NFCONT_3:29
for X, X1 being set
for S being RealNormSpace
for f1, f2 being PartFunc of REAL, the carrier of S st f1 | X is Lipschitzian &amp; f2 | X1 is Lipschitzian holds
(f1 - f2) | (X /\ X1) is Lipschitzian
proofend;

registration
let S be RealNormSpace;
let f be Lipschitzian PartFunc of REAL, the carrier of S;
let p be Real;
clusterp (#) f ->  Lipschitzian for PartFunc of REAL, the carrier of S;
coherence
 for b1 being PartFunc of REAL, the carrier of S st b1 = p (#) f holds
b1 is Lipschitzian
proofend;
end;

theorem :: NFCONT_3:30
for X being set
for p being Real
for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S st f | X is Lipschitzian &amp; X c= dom f holds
(p (#) f) | X is Lipschitzian
proofend;

registration
let S be RealNormSpace;
let f be Lipschitzian PartFunc of REAL, the carrier of S;
cluster||.f.|| ->  Lipschitzian for PartFunc of REAL,REAL;
coherence
 for b1 being PartFunc of REAL,REAL st b1 = ||.f.|| holds
b1 is Lipschitzian
proofend;
end;

theorem :: NFCONT_3:31
for X being set
for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S st f | X is Lipschitzian holds
( - (f | X) is Lipschitzian &amp; (- f) | X is Lipschitzian &amp; ||.f.|| | X is Lipschitzian )
proofend;

registration
let S be RealNormSpace;
cluster Function-like constant  ->  Lipschitzian for Element of bool [:REAL, the carrier of S:];
coherence
 for b1 being PartFunc of REAL, the carrier of S st b1 is constant holds
b1 is Lipschitzian
proofend;
end;

registration
let S be RealNormSpace;
cluster Function-like Lipschitzian  ->  continuous for Element of bool [:REAL, the carrier of S:];
coherence
 for b1 being PartFunc of REAL, the carrier of S st b1 is Lipschitzian holds
b1 is continuous
proofend;
end;

theorem :: NFCONT_3:32
for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S st ex r being Point of S st rng f = {r} holds
f is continuous
proofend;

theorem :: NFCONT_3:33
for X being set
for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S
for r, p being Point of S st ( for x0 being real number st x0 in X holds
f /. x0 = (x0 * r) + p ) holds
f | X is continuous
proofend;