:: More on the Continuity of Real Functions
:: by Keiko Narita , Artur Kornilowicz and Yasunari Shidama
::
:: Received February 22, 2011
:: Copyright (c) 2011-2012 Association of Mizar Users


begin

definition
let n be Element of NAT ;
let f be PartFunc of REAL,(REAL n);
let x0 be real number ;
predf is_continuous_in x0 means :Def1: :: NFCONT_4:def 1
 ex g being PartFunc of REAL,(REAL-NS n) st
( f = g & g is_continuous_in x0 );
end;

:: deftheorem Def1 defines is_continuous_in NFCONT_4:def_1_:_
 for n being Element of NAT
for f being PartFunc of REAL,(REAL n)
for x0 being real number holds
( f is_continuous_in x0 iff ex g being PartFunc of REAL,(REAL-NS n) st
( f = g & g is_continuous_in x0 ) );

theorem Th1: :: NFCONT_4:1
for n being Element of NAT
for x0 being real number
for f being PartFunc of REAL,(REAL n)
for h being PartFunc of REAL,(REAL-NS n) st h = f holds
( f is_continuous_in x0 iff h is_continuous_in x0 )
proofend;

theorem Th2: :: NFCONT_4:2
for n being Element of NAT
for X being set
for x0 being real number
for f being PartFunc of REAL,(REAL n) st x0 in X & f is_continuous_in x0 holds
f | X is_continuous_in x0
proofend;

theorem Th3: :: NFCONT_4:3
for n being Element of NAT
for x0 being real number
for f being PartFunc of REAL,(REAL n) 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 Th4: :: NFCONT_4:4
for n being Element of NAT
for r being Real
for z being Element of REAL n
for w being 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  }
proofend;

definition
let n be Element of NAT ;
let Z be set ;
let f be PartFunc of Z,(REAL n);
deffunc H1( set ) ->  Element of REAL = |.(f /. $1).|;
func|.f.| ->  PartFunc of Z,REAL means :Def2: :: NFCONT_4:def 2
( dom it = dom f &amp; ( for x being set st x in dom it holds
it /. x = |.(f /. x).| ) );
existence
 ex b1 being PartFunc of Z,REAL st
( dom b1 = dom f &amp; ( for x being set st x in dom b1 holds
b1 /. x = |.(f /. x).| ) )
proofend;
uniqueness
 for b1, b2 being PartFunc of Z,REAL st dom b1 = dom f &amp; ( for x being set st x in dom b1 holds
b1 /. x = |.(f /. x).| ) &amp; dom b2 = dom f &amp; ( for x being set st x in dom b2 holds
b2 /. x = |.(f /. x).| ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines |. NFCONT_4:def_2_:_
 for n being Element of NAT
for Z being set
for f being PartFunc of Z,(REAL n)
for b4 being PartFunc of Z,REAL holds
( b4 = |.f.| iff ( dom b4 = dom f &amp; ( for x being set st x in dom b4 holds
b4 /. x = |.(f /. x).| ) ) );

definition
let n be Element of NAT ;
let Z be non empty set ;
let f be PartFunc of Z,(REAL n);
deffunc H1( set ) ->  M13( REAL , REAL n) = - (f /. $1);
defpred S1[ set ] means $1 in dom f;
func - f ->  PartFunc of Z,(REAL n) means :Def3: :: NFCONT_4:def 3
( dom it = dom f &amp; ( for c being set st c in dom it holds
it /. c = - (f /. c) ) );
existence
 ex b1 being PartFunc of Z,(REAL n) st
( dom b1 = dom f &amp; ( for c being set st c in dom b1 holds
b1 /. c = - (f /. c) ) )
proofend;
uniqueness
 for b1, b2 being PartFunc of Z,(REAL n) st dom b1 = dom f &amp; ( for c being set st c in dom b1 holds
b1 /. c = - (f /. c) ) &amp; dom b2 = dom f &amp; ( for c being set st c in dom b2 holds
b2 /. c = - (f /. c) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines - NFCONT_4:def_3_:_
 for n being Element of NAT
for Z being non empty set
for f, b4 being PartFunc of Z,(REAL n) holds
( b4 = - f iff ( dom b4 = dom f &amp; ( for c being set st c in dom b4 holds
b4 /. c = - (f /. c) ) ) );

theorem Th5: :: NFCONT_4:5
for n being Element of NAT
for W being non empty set
for f1, f2 being PartFunc of W,(REAL-NS n)
for g1, g2 being PartFunc of W,(REAL n) st f1 = g1 &amp; f2 = g2 holds
f1 + f2 = g1 + g2
proofend;

theorem Th6: :: NFCONT_4:6
for n being Element of NAT
for W being non empty set
for f1 being PartFunc of W,(REAL-NS n)
for g1 being PartFunc of W,(REAL n)
for a being Real st f1 = g1 holds
a (#) f1 = a (#) g1
proofend;

theorem :: NFCONT_4:7
for n being Element of NAT
for W being non empty set
for f1 being PartFunc of W,(REAL n) holds (- 1) (#) f1 = - f1
proofend;

theorem Th8: :: NFCONT_4:8
for n being Element of NAT
for W being non empty set
for f1 being PartFunc of W,(REAL-NS n)
for g1 being PartFunc of W,(REAL n) st f1 = g1 holds
- f1 = - g1
proofend;

theorem Th9: :: NFCONT_4:9
for n being Element of NAT
for W being non empty set
for f1 being PartFunc of W,(REAL-NS n)
for g1 being PartFunc of W,(REAL n) st f1 = g1 holds
||.f1.|| = |.g1.|
proofend;

theorem Th10: :: NFCONT_4:10
for n being Element of NAT
for W being non empty set
for f1, f2 being PartFunc of W,(REAL-NS n)
for g1, g2 being PartFunc of W,(REAL n) st f1 = g1 &amp; f2 = g2 holds
f1 - f2 = g1 - g2
proofend;

theorem :: NFCONT_4:11
for n being Element of NAT
for x0 being real number
for f being PartFunc of REAL,(REAL n) holds
( f is_continuous_in x0 iff ( x0 in dom f &amp; ( for N1 being Subset of (REAL n) st ex r being Real st
( 0 < r &amp;  {  y where y is Element of REAL n : |.(y - (f /. x0)).| < r  }  = N1 ) holds
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 :: NFCONT_4:12
for n being Element of NAT
for x0 being real number
for f being PartFunc of REAL,(REAL n) holds
( f is_continuous_in x0 iff ( x0 in dom f &amp; ( for N1 being Subset of (REAL n) st ex r being Real st
( 0 < r &amp;  {  y where y is Element of REAL n : |.(y - (f /. x0)).| < r  }  = N1 ) holds
ex N being Neighbourhood of x0 st f .: N c= N1 ) ) )
proofend;

theorem :: NFCONT_4:13
for n being Element of NAT
for x0 being real number
for f being PartFunc of REAL,(REAL n) st ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} holds
f is_continuous_in x0
proofend;

theorem :: NFCONT_4:14
for n being Element of NAT
for x0 being real number
for f1, f2 being PartFunc of REAL,(REAL n) 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
proofend;

theorem :: NFCONT_4:15
for n being Element of NAT
for x0 being real number
for f1, f2 being PartFunc of REAL,(REAL n) 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
proofend;

theorem :: NFCONT_4:16
for n being Element of NAT
for r being Real
for x0 being real number
for f being PartFunc of REAL,(REAL n) st f is_continuous_in x0 holds
r (#) f is_continuous_in x0
proofend;

theorem :: NFCONT_4:17
for n being Element of NAT
for x0 being real number
for f being PartFunc of REAL,(REAL n) st x0 in dom f &amp; f is_continuous_in x0 holds
|.f.| is_continuous_in x0
proofend;

theorem :: NFCONT_4:18
for n being Element of NAT
for x0 being real number
for f being PartFunc of REAL,(REAL n) st x0 in dom f &amp; f is_continuous_in x0 holds
- f is_continuous_in x0
proofend;

theorem :: NFCONT_4:19
for n being Element of NAT
for x0 being real number
for S being RealNormSpace
for z being Point of (REAL-NS n)
for f1 being PartFunc of REAL,(REAL n)
for f2 being PartFunc of (REAL-NS n),S st x0 in dom (f2 * f1) &amp; f1 is_continuous_in x0 &amp; z = f1 /. x0 &amp; f2 is_continuous_in z holds
f2 * f1 is_continuous_in x0
proofend;

theorem Th20: :: NFCONT_4:20
for x0 being real number
for S being RealNormSpace
for f1 being PartFunc of REAL,S
for f2 being PartFunc of S,REAL 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 n be Element of NAT ;
let f be PartFunc of (REAL n),REAL;
let x0 be Element of REAL n;
predf is_continuous_in x0 means :Def4: :: NFCONT_4:def 4
 ex y0 being Point of (REAL-NS n) ex g being PartFunc of (REAL-NS n),REAL st
( x0 = y0 &amp; f = g &amp; g is_continuous_in y0 );
end;

:: deftheorem Def4 defines is_continuous_in NFCONT_4:def_4_:_
 for n being Element of NAT
for f being PartFunc of (REAL n),REAL
for x0 being Element of REAL n holds
( f is_continuous_in x0 iff ex y0 being Point of (REAL-NS n) ex g being PartFunc of (REAL-NS n),REAL st
( x0 = y0 &amp; f = g &amp; g is_continuous_in y0 ) );

theorem Th21: :: NFCONT_4:21
for n being Element of NAT
for f being PartFunc of (REAL n),REAL
for h being PartFunc of (REAL-NS n),REAL
for x0 being Element of REAL n
for y0 being Point of (REAL-NS n) st f = h &amp; x0 = y0 holds
( f is_continuous_in x0 iff h is_continuous_in y0 )
proofend;

theorem Th22: :: NFCONT_4:22
for n being Element of NAT
for x0 being real number
for f1 being PartFunc of REAL,(REAL n)
for f2 being PartFunc of (REAL n),REAL 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 n be Element of NAT ;
let f be PartFunc of REAL,(REAL n);
attrf is continuous  means :Def5: :: NFCONT_4:def 5
 for x0 being real number st x0 in dom f holds
f is_continuous_in x0;
end;

:: deftheorem Def5 defines continuous NFCONT_4:def_5_:_
 for n being Element of NAT
for f being PartFunc of REAL,(REAL n) holds
( f is continuous iff for x0 being real number st x0 in dom f holds
f is_continuous_in x0 );

theorem Th23: :: NFCONT_4:23
for n being Element of NAT
for g being PartFunc of REAL,(REAL-NS n)
for f being PartFunc of REAL,(REAL n) st g = f holds
( g is continuous iff f is continuous )
proofend;

theorem Th24: :: NFCONT_4:24
for n being Element of NAT
for X being set
for f being PartFunc of REAL,(REAL n) 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 n be Element of NAT ;
cluster Function-like constant  ->  continuous for Element of bool [:REAL,(REAL n):];
coherence
 for b1 being PartFunc of REAL,(REAL n) st b1 is constant holds
b1 is continuous
proofend;
end;

registration
let n be Element of NAT ;
cluster Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() continuous for Element of bool [:REAL,(REAL n):];
existence
 ex b1 being PartFunc of REAL,(REAL n) st b1 is continuous
proofend;
end;

registration
let n be Element of NAT ;
let f be continuous PartFunc of REAL,(REAL n);
let X be set ;
clusterf | X ->  continuous for PartFunc of REAL,(REAL n);
coherence
 for b1 being PartFunc of REAL,(REAL n) st b1 = f | X holds
b1 is continuous
proofend;
end;

theorem :: NFCONT_4:25
for n being Element of NAT
for X, X1 being set
for f being PartFunc of REAL,(REAL n) st f | X is continuous &amp; X1 c= X holds
f | X1 is continuous
proofend;

registration
let n be Element of NAT ;
cluster empty Function-like  ->  continuous for Element of bool [:REAL,(REAL n):];
coherence
 for b1 being PartFunc of REAL,(REAL n) st b1 is empty holds
b1 is continuous ;
end;

registration
let n be Element of NAT ;
let f be PartFunc of REAL,(REAL n);
let X be trivial set ;
clusterf | X ->  continuous for PartFunc of REAL,(REAL n);
coherence
 for b1 being PartFunc of REAL,(REAL n) st b1 = f | X holds
b1 is continuous
proofend;
end;

registration
let n be Element of NAT ;
let f1, f2 be continuous PartFunc of REAL,(REAL n);
clusterf1 + f2 ->  continuous for PartFunc of REAL,(REAL n);
coherence
 for b1 being PartFunc of REAL,(REAL n) st b1 = f1 + f2 holds
b1 is continuous
proofend;
end;

theorem :: NFCONT_4:26
for n being Element of NAT
for X being set
for f1, f2 being PartFunc of REAL,(REAL n) 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_4:27
for n being Element of NAT
for X, X1 being set
for f1, f2 being PartFunc of REAL,(REAL n) 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 n be Element of NAT ;
let f be continuous PartFunc of REAL,(REAL n);
let r be Real;
clusterr (#) f ->  continuous for PartFunc of REAL,(REAL n);
coherence
 for b1 being PartFunc of REAL,(REAL n) st b1 = r (#) f holds
b1 is continuous
proofend;
end;

theorem :: NFCONT_4:28
for n being Element of NAT
for X being set
for r being Real
for f being PartFunc of REAL,(REAL n) st X c= dom f &amp; f | X is continuous holds
(r (#) f) | X is continuous
proofend;

theorem :: NFCONT_4:29
for n being Element of NAT
for X being set
for f being PartFunc of REAL,(REAL n) st X c= dom f &amp; f | X is continuous holds
( |.f.| | X is continuous &amp; (- f) | X is continuous )
proofend;

theorem :: NFCONT_4:30
for n being Element of NAT
for f being PartFunc of REAL,(REAL n) 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 :: NFCONT_4:31
for n being Element of NAT
for f being PartFunc of REAL,(REAL n)
for Y being Subset of (REAL-NS n) st dom f is compact &amp; f | (dom f) is continuous &amp; Y = rng f holds
Y is compact
proofend;

theorem :: NFCONT_4:32
for n being Element of NAT
for f being PartFunc of REAL,(REAL n)
for Y being Subset of REAL
for Z being Subset of (REAL-NS n) st Y c= dom f &amp; Z = f .: Y &amp; Y is compact &amp; f | Y is continuous holds
Z is compact
proofend;

definition
let n be Element of NAT ;
let f be PartFunc of REAL,(REAL n);
attrf is Lipschitzian  means :Def6: :: NFCONT_4:def 6
 ex g being PartFunc of REAL,(REAL-NS n) st
( g = f &amp; g is Lipschitzian );
end;

:: deftheorem Def6 defines Lipschitzian NFCONT_4:def_6_:_
 for n being Element of NAT
for f being PartFunc of REAL,(REAL n) holds
( f is Lipschitzian iff ex g being PartFunc of REAL,(REAL-NS n) st
( g = f &amp; g is Lipschitzian ) );

theorem Th33: :: NFCONT_4:33
for n being Element of NAT
for f being PartFunc of REAL,(REAL n) 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)) ) ) )
proofend;

theorem Th34: :: NFCONT_4:34
for n being Element of NAT
for f being PartFunc of REAL,(REAL n)
for h being PartFunc of REAL,(REAL-NS n) st f = h holds
( f is Lipschitzian iff h is Lipschitzian )
proofend;

theorem :: NFCONT_4:35
for n being Element of NAT
for X being set
for f being PartFunc of REAL,(REAL n) 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 n be Element of NAT ;
cluster empty Function-like  ->  Lipschitzian for Element of bool [:REAL,(REAL n):];
coherence
 for b1 being PartFunc of REAL,(REAL n) st b1 is empty holds
b1 is Lipschitzian
proofend;
end;

registration
let n be Element of NAT ;
cluster empty Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() for Element of bool [:REAL,(REAL n):];
existence
 ex b1 being PartFunc of REAL,(REAL n) st b1 is empty
proofend;
end;

registration
let n be Element of NAT ;
let f be Lipschitzian PartFunc of REAL,(REAL n);
let X be set ;
clusterf | X ->  Lipschitzian for PartFunc of REAL,(REAL n);
coherence
 for b1 being PartFunc of REAL,(REAL n) st b1 = f | X holds
b1 is Lipschitzian
proofend;
end;

theorem :: NFCONT_4:36
for n being Element of NAT
for X, X1 being set
for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian &amp; X1 c= X holds
f | X1 is Lipschitzian
proofend;

registration
let n be Element of NAT ;
let f1, f2 be Lipschitzian PartFunc of REAL,(REAL n);
clusterf1 + f2 ->  Lipschitzian for PartFunc of REAL,(REAL n);
coherence
 for b1 being PartFunc of REAL,(REAL n) st b1 = f1 + f2 holds
b1 is Lipschitzian
proofend;
clusterf1 - f2 ->  Lipschitzian for PartFunc of REAL,(REAL n);
coherence
 for b1 being PartFunc of REAL,(REAL n) st b1 = f1 - f2 holds
b1 is Lipschitzian
proofend;
end;

theorem :: NFCONT_4:37
for n being Element of NAT
for X, X1 being set
for f1, f2 being PartFunc of REAL,(REAL n) st f1 | X is Lipschitzian &amp; f2 | X1 is Lipschitzian holds
(f1 + f2) | (X /\ X1) is Lipschitzian
proofend;

theorem :: NFCONT_4:38
for n being Element of NAT
for X, X1 being set
for f1, f2 being PartFunc of REAL,(REAL n) st f1 | X is Lipschitzian &amp; f2 | X1 is Lipschitzian holds
(f1 - f2) | (X /\ X1) is Lipschitzian
proofend;

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

theorem :: NFCONT_4:39
for n being Element of NAT
for X being set
for p being Real
for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian &amp; X c= dom f holds
(p (#) f) | X is Lipschitzian
proofend;

registration
let n be Element of NAT ;
let f be Lipschitzian PartFunc of REAL,(REAL n);
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_4:40
for n being Element of NAT
for X being set
for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian holds
( - (f | X) is Lipschitzian &amp; |.f.| | X is Lipschitzian &amp; (- f) | X is Lipschitzian )
proofend;

registration
let n be Element of NAT ;
cluster Function-like constant  ->  Lipschitzian for Element of bool [:REAL,(REAL n):];
coherence
 for b1 being PartFunc of REAL,(REAL n) st b1 is constant holds
b1 is Lipschitzian
proofend;
end;

registration
let n be Element of NAT ;
cluster Function-like Lipschitzian  ->  continuous for Element of bool [:REAL,(REAL n):];
coherence
 for b1 being PartFunc of REAL,(REAL n) st b1 is Lipschitzian holds
b1 is continuous
proofend;
end;

theorem :: NFCONT_4:41
for n being Element of NAT
for X being set
for f being PartFunc of REAL,(REAL n)
for r, p being Element of REAL n st ( for x0 being real number st x0 in X holds
f /. x0 = (x0 * r) + p ) holds
f | X is continuous
proofend;

theorem Th42: :: NFCONT_4:42
for n, i being Element of NAT
for x0 being Element of REAL n st 1 <= i &amp; i <= n holds
proj (i,n) is_continuous_in x0
proofend;

theorem Th43: :: NFCONT_4:43
for x0 being real number
for n being non empty Element of NAT
for h being PartFunc of REAL,(REAL n) holds
( h is_continuous_in x0 iff ( x0 in dom h &amp; ( for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is_continuous_in x0 ) ) )
proofend;

theorem :: NFCONT_4:44
for n being non empty Element of NAT
for h being PartFunc of REAL,(REAL n) holds
( h is continuous iff for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is continuous )
proofend;

theorem Th45: :: NFCONT_4:45
for n, i being Element of NAT
for x0 being Point of (REAL-NS n) st 1 <= i &amp; i <= n holds
Proj (i,n) is_continuous_in x0
proofend;

theorem Th46: :: NFCONT_4:46
for x0 being real number
for n being non empty Element of NAT
for h being PartFunc of REAL,(REAL-NS n) holds
( h is_continuous_in x0 iff for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is_continuous_in x0 )
proofend;

theorem :: NFCONT_4:47
for n being non empty Element of NAT
for h being PartFunc of REAL,(REAL-NS n) holds
( h is continuous iff for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is continuous )
proofend;