:: 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 ;
pred f 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 )
proof end;

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
proof end;

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 & ( for r being Real st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) )
proof end;

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 }
proof end;

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 & ( 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 & ( for x being set st x in dom b1 holds
b1 /. x = |.(f /. x).| ) )
proof end;
uniqueness
for b1, b2 being PartFunc of Z,REAL st dom b1 = dom f & ( for x being set st x in dom b1 holds
b1 /. x = |.(f /. x).| ) & dom b2 = dom f & ( for x being set st x in dom b2 holds
b2 /. x = |.(f /. x).| ) holds
b1 = b2
proof end;
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 & ( 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 & ( 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 & ( for c being set st c in dom b1 holds
b1 /. c = - (f /. c) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of Z,(REAL n) st dom b1 = dom f & ( for c being set st c in dom b1 holds
b1 /. c = - (f /. c) ) & dom b2 = dom f & ( for c being set st c in dom b2 holds
b2 /. c = - (f /. c) ) holds
b1 = b2
proof end;
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 & ( 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 & f2 = g2 holds
f1 + f2 = g1 + g2
proof end;

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
proof end;

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
proof end;

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
proof end;

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.|
proof end;

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 & f2 = g2 holds
f1 - f2 = g1 - g2
proof end;

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 & ( for N1 being Subset of (REAL n) st ex r being Real st
( 0 < r & { 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 & x1 in N holds
f /. x1 in N1 ) ) )
proof end;

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 & ( for N1 being Subset of (REAL n) st ex r being Real st
( 0 < r & { 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 ) ) )
proof end;

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
proof end;

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) & f1 is_continuous_in x0 & f2 is_continuous_in x0 holds
f1 + f2 is_continuous_in x0
proof end;

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) & f1 is_continuous_in x0 & f2 is_continuous_in x0 holds
f1 - f2 is_continuous_in x0
proof end;

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
proof end;

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 & f is_continuous_in x0 holds
|.f.| is_continuous_in x0
proof end;

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 & f is_continuous_in x0 holds
- f is_continuous_in x0
proof end;

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) & f1 is_continuous_in x0 & z = f1 /. x0 & f2 is_continuous_in z holds
f2 * f1 is_continuous_in x0
proof end;

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) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds
f2 * f1 is_continuous_in x0
proof end;

definition
let n be Element of NAT ;
let f be PartFunc of (REAL n),REAL;
let x0 be Element of REAL n;
pred f 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 & f = g & 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 & f = g & 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 & x0 = y0 holds
( f is_continuous_in x0 iff h is_continuous_in y0 )
proof end;

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) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds
f2 * f1 is_continuous_in x0
proof end;

definition
let n be Element of NAT ;
let f be PartFunc of REAL,(REAL n);
attr f 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 )
proof end;

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 & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) )
proof end;

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
proof end;
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
proof end;
end;

registration
let n be Element of NAT ;
let f be continuous PartFunc of REAL,(REAL n);
let X be set ;
cluster f | 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
proof end;
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 & X1 c= X holds
f | X1 is continuous
proof end;

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 ;
cluster f | 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
proof end;
end;

registration
let n be Element of NAT ;
let f1, f2 be continuous PartFunc of REAL,(REAL n);
cluster f1 + 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
proof end;
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) & f1 | X is continuous & f2 | X is continuous holds
( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous )
proof end;

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 & 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 )
proof end;

registration
let n be Element of NAT ;
let f be continuous PartFunc of REAL,(REAL n);
let r be Real;
cluster r (#) 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
proof end;
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 & f | X is continuous holds
(r (#) f) | X is continuous
proof end;

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 & f | X is continuous holds
( |.f.| | X is continuous & (- f) | X is continuous )
proof end;

theorem :: NFCONT_4:30
for n being Element of NAT
for f being PartFunc of REAL,(REAL n) st f is total & ( for x1, x2 being real number holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being real number st f is_continuous_in x0 holds
f | REAL is continuous
proof end;

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 & f | (dom f) is continuous & Y = rng f holds
Y is compact
proof end;

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 & Z = f .: Y & Y is compact & f | Y is continuous holds
Z is compact
proof end;

definition
let n be Element of NAT ;
let f be PartFunc of REAL,(REAL n);
attr f is Lipschitzian means :Def6: :: NFCONT_4:def 6
ex g being PartFunc of REAL,(REAL-NS n) st
( g = f & 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 & 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 & ( for x1, x2 being real number st x1 in dom f & x2 in dom f holds
|.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) ) )
proof end;

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 )
proof end;

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 & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
|.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) ) )
proof end;

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
proof end;
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
proof end;
end;

registration
let n be Element of NAT ;
let f be Lipschitzian PartFunc of REAL,(REAL n);
let X be set ;
cluster f | 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
proof end;
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 & X1 c= X holds
f | X1 is Lipschitzian
proof end;

registration
let n be Element of NAT ;
let f1, f2 be Lipschitzian PartFunc of REAL,(REAL n);
cluster f1 + 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
proof end;
cluster f1 - 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
proof end;
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 & f2 | X1 is Lipschitzian holds
(f1 + f2) | (X /\ X1) is Lipschitzian
proof end;

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 & f2 | X1 is Lipschitzian holds
(f1 - f2) | (X /\ X1) is Lipschitzian
proof end;

registration
let n be Element of NAT ;
let f be Lipschitzian PartFunc of REAL,(REAL n);
let p be Real;
cluster p (#) 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
proof end;
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 & X c= dom f holds
(p (#) f) | X is Lipschitzian
proof end;

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
proof end;
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 & |.f.| | X is Lipschitzian & (- f) | X is Lipschitzian )
proof end;

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
proof end;
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
proof end;
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
proof end;

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

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 & ( for i being Element of NAT st i in Seg n holds
(proj (i,n)) * h is_continuous_in x0 ) ) )
proof end;

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 )
proof end;

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

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 )
proof end;

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 )
proof end;