:: Real Function Continuity
::
:: Copyright (c) 1990-2021 Association of Mizar Users

definition
let f be PartFunc of REAL,REAL;
let x0 be Real;
pred f is_continuous_in x0 means :: FCONT_1:def 1
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 defines is_continuous_in FCONT_1:def 1 :
for f being PartFunc of REAL,REAL
for x0 being Real holds
( f is_continuous_in x0 iff 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 Th1: :: FCONT_1:1
for X being set
for x0 being Real
for f being PartFunc of REAL,REAL st x0 in X & f is_continuous_in x0 holds
f | X is_continuous_in x0
proof end;

theorem :: FCONT_1:2
for x0 being Real
for f being PartFunc of REAL,REAL holds
( f is_continuous_in x0 iff for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Nat holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f . x0 = lim (f /* s1) ) )
proof end;

theorem Th3: :: FCONT_1:3
for x0 being Real
for f being PartFunc of REAL,REAL holds
( f is_continuous_in x0 iff for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < s holds
|.((f . x1) - (f . x0)).| < r ) ) )
proof end;

theorem Th4: :: FCONT_1:4
for f being PartFunc of REAL,REAL
for x0 being Real holds
( f is_continuous_in x0 iff for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st
for x1 being Real st x1 in dom f & x1 in N holds
f . x1 in N1 )
proof end;

theorem Th5: :: FCONT_1:5
for f being PartFunc of REAL,REAL
for x0 being Real holds
( f is_continuous_in x0 iff for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st f .: N c= N1 )
proof end;

theorem :: FCONT_1:6
for x0 being Real
for f being PartFunc of REAL,REAL st ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} holds
f is_continuous_in x0
proof end;

theorem Th7: :: FCONT_1:7
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 holds
( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 & f1 (#) f2 is_continuous_in x0 )
proof end;

theorem Th8: :: FCONT_1:8
for r, x0 being Real
for f being PartFunc of REAL,REAL st x0 in dom f & f is_continuous_in x0 holds
r (#) f is_continuous_in x0
proof end;

theorem :: FCONT_1:9
for x0 being Real
for f being PartFunc of REAL,REAL st x0 in dom f & f is_continuous_in x0 holds
( abs f is_continuous_in x0 & - f is_continuous_in x0 )
proof end;

theorem Th10: :: FCONT_1:10
for x0 being Real
for f being PartFunc of REAL,REAL st f is_continuous_in x0 & f . x0 <> 0 holds
f ^ is_continuous_in x0
proof end;

theorem :: FCONT_1:11
for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st x0 in dom f2 & f1 is_continuous_in x0 & f1 . x0 <> 0 & f2 is_continuous_in x0 holds
f2 / f1 is_continuous_in x0
proof end;

theorem Th12: :: FCONT_1:12
for x0 being Real
for f1, f2 being PartFunc of REAL,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 f be PartFunc of REAL,REAL;
attr f is continuous means :Def2: :: FCONT_1:def 2
for x0 being Real st x0 in dom f holds
f is_continuous_in x0;
end;

:: deftheorem Def2 defines continuous FCONT_1:def 2 :
for f being PartFunc of REAL,REAL holds
( f is continuous iff for x0 being Real st x0 in dom f holds
f is_continuous_in x0 );

theorem Th13: :: FCONT_1:13
for X being set
for f being PartFunc of REAL,REAL st X c= dom f holds
( f | X is continuous iff for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds
( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) ) )
proof end;

theorem Th14: :: FCONT_1:14
for X being set
for f being PartFunc of REAL,REAL st X c= dom f holds
( f | X is continuous iff for x0, r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in X & |.(x1 - x0).| < s holds
|.((f . x1) - (f . x0)).| < r ) ) )
proof end;

registration
coherence
for b1 being PartFunc of REAL,REAL st b1 is V8() holds
b1 is continuous
proof end;
end;

registration
existence
ex b1 being PartFunc of REAL,REAL st b1 is continuous
proof end;
end;

registration
let f be continuous PartFunc of REAL,REAL;
let X be set ;
cluster f | X -> continuous for PartFunc of REAL,REAL;
coherence
for b1 being PartFunc of REAL,REAL st b1 = f | X holds
b1 is continuous
proof end;
end;

theorem :: FCONT_1:15
for X being set
for f being PartFunc of REAL,REAL holds
( f | X is continuous iff (f | X) | X is continuous ) ;

theorem Th16: :: FCONT_1:16
for X, X1 being set
for f being PartFunc of REAL,REAL st f | X is continuous & X1 c= X holds
f | X1 is continuous
proof end;

registration
coherence
for b1 being PartFunc of REAL,REAL st b1 is empty holds
b1 is continuous
;
end;

registration
let f be PartFunc of REAL,REAL;
let X be trivial set ;
cluster f | X -> continuous for PartFunc of REAL,REAL;
coherence
for b1 being PartFunc of REAL,REAL st b1 = f | X holds
b1 is continuous
proof end;
end;

theorem :: FCONT_1:17
for x0 being Real
for f being PartFunc of REAL,REAL holds f | {x0} is continuous ;

registration
let f1, f2 be continuous PartFunc of REAL,REAL;
cluster f1 + f2 -> continuous for PartFunc of REAL,REAL;
coherence
for b1 being PartFunc of REAL,REAL st b1 = f1 + f2 holds
b1 is continuous
proof end;
cluster f1 - f2 -> continuous for PartFunc of REAL,REAL;
coherence
for b1 being PartFunc of REAL,REAL st b1 = f1 - f2 holds
b1 is continuous
proof end;
cluster f1 (#) f2 -> continuous for PartFunc of REAL,REAL;
coherence
for b1 being PartFunc of REAL,REAL st b1 = f1 (#) f2 holds
b1 is continuous
proof end;
end;

theorem Th18: :: FCONT_1:18
for X being set
for f1, f2 being PartFunc of REAL,REAL 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 & (f1 (#) f2) | X is continuous )
proof end;

theorem :: FCONT_1:19
for X, X1 being set
for f1, f2 being PartFunc of REAL,REAL 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 & (f1 (#) f2) | (X /\ X1) is continuous )
proof end;

registration
let f be continuous PartFunc of REAL,REAL;
let r be Real;
cluster r (#) f -> continuous for PartFunc of REAL,REAL;
coherence
for b1 being PartFunc of REAL,REAL st b1 = r (#) f holds
b1 is continuous
proof end;
end;

theorem Th20: :: FCONT_1:20
for r being Real
for X being set
for f being PartFunc of REAL,REAL st X c= dom f & f | X is continuous holds
(r (#) f) | X is continuous
proof end;

theorem :: FCONT_1:21
for X being set
for f being PartFunc of REAL,REAL st X c= dom f & f | X is continuous holds
( (abs f) | X is continuous & (- f) | X is continuous )
proof end;

theorem Th22: :: FCONT_1:22
for X being set
for f being PartFunc of REAL,REAL st f | X is continuous & f " = {} holds
(f ^) | X is continuous
proof end;

theorem :: FCONT_1:23
for X being set
for f being PartFunc of REAL,REAL st f | X is continuous & (f | X) " = {} holds
(f ^) | X is continuous
proof end;

theorem :: FCONT_1:24
for X being set
for f1, f2 being PartFunc of REAL,REAL st X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f1 " = {} & f2 | X is continuous holds
(f2 / f1) | X is continuous
proof end;

registration
let f1, f2 be continuous PartFunc of REAL,REAL;
cluster f1 (#) f2 -> continuous for PartFunc of REAL,REAL;
coherence
for b1 being PartFunc of REAL,REAL st b1 = f2 * f1 holds
b1 is continuous
proof end;
end;

theorem :: FCONT_1:25
for X being set
for f1, f2 being PartFunc of REAL,REAL st f1 | X is continuous & f2 | (f1 .: X) is continuous holds
(f2 * f1) | X is continuous
proof end;

theorem :: FCONT_1:26
for X, X1 being set
for f1, f2 being PartFunc of REAL,REAL st f1 | X is continuous & f2 | X1 is continuous holds
(f2 * f1) | (X /\ (f1 " X1)) is continuous
proof end;

theorem :: FCONT_1:27
for f being PartFunc of REAL,REAL st f is total & ( for x1, x2 being Real holds f . (x1 + x2) = (f . x1) + (f . x2) ) & ex x0 being Real st f is_continuous_in x0 holds
f | REAL is continuous
proof end;

theorem Th28: :: FCONT_1:28
for f being PartFunc of REAL,REAL st dom f is compact & f | (dom f) is continuous holds
rng f is compact
proof end;

theorem :: FCONT_1:29
for Y being Subset of REAL
for f being PartFunc of REAL,REAL st Y c= dom f & Y is compact & f | Y is continuous holds
f .: Y is compact
proof end;

theorem Th30: :: FCONT_1:30
for f being PartFunc of REAL,REAL st dom f <> {} & dom f is compact & f | (dom f) is continuous holds
ex x1, x2 being Real st
( x1 in dom f & x2 in dom f & f . x1 = upper_bound (rng f) & f . x2 = lower_bound (rng f) )
proof end;

:: Extreme value theorem
theorem :: FCONT_1:31
for f being PartFunc of REAL,REAL
for Y being Subset of REAL st Y <> {} & Y c= dom f & Y is compact & f | Y is continuous holds
ex x1, x2 being Real st
( x1 in Y & x2 in Y & f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) )
proof end;

definition
let f be PartFunc of REAL,REAL;
attr f is Lipschitzian means :Def3: :: FCONT_1:def 3
ex r being Real st
( 0 < r & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= r * |.(x1 - x2).| ) );
end;

:: deftheorem Def3 defines Lipschitzian FCONT_1:def 3 :
for f being PartFunc of REAL,REAL holds
( f is Lipschitzian iff ex r being Real st
( 0 < r & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= r * |.(x1 - x2).| ) ) );

theorem Th32: :: FCONT_1:32
for X being set
for f being PartFunc of REAL,REAL holds
( f | X is Lipschitzian iff ex r being Real st
( 0 < r & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) holds
|.((f . x1) - (f . x2)).| <= r * |.(x1 - x2).| ) ) )
proof end;

registration
coherence
for b1 being PartFunc of REAL,REAL st b1 is empty holds
b1 is Lipschitzian
proof end;
end;

registration
existence
ex b1 being PartFunc of REAL,REAL st b1 is empty
proof end;
end;

registration
let f be Lipschitzian PartFunc of REAL,REAL;
let X be set ;
cluster f | X -> Lipschitzian for PartFunc of REAL,REAL;
coherence
for b1 being PartFunc of REAL,REAL st b1 = f | X holds
b1 is Lipschitzian
proof end;
end;

theorem :: FCONT_1:33
for X, X1 being set
for f being PartFunc of REAL,REAL st f | X is Lipschitzian & X1 c= X holds
f | X1 is Lipschitzian
proof end;

registration
let f1, f2 be Lipschitzian PartFunc of REAL,REAL;
cluster f1 + f2 -> Lipschitzian for PartFunc of REAL,REAL;
coherence
for b1 being PartFunc of REAL,REAL st b1 = f1 + f2 holds
b1 is Lipschitzian
proof end;
cluster f1 - f2 -> Lipschitzian for PartFunc of REAL,REAL;
coherence
for b1 being PartFunc of REAL,REAL st b1 = f1 - f2 holds
b1 is Lipschitzian
proof end;
end;

theorem :: FCONT_1:34
for X, X1 being set
for f1, f2 being PartFunc of REAL,REAL st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds
(f1 + f2) | (X /\ X1) is Lipschitzian
proof end;

theorem :: FCONT_1:35
for X, X1 being set
for f1, f2 being PartFunc of REAL,REAL st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds
(f1 - f2) | (X /\ X1) is Lipschitzian
proof end;

registration
let f1, f2 be bounded Lipschitzian PartFunc of REAL,REAL;
cluster f1 (#) f2 -> Lipschitzian for PartFunc of REAL,REAL;
coherence
for b1 being PartFunc of REAL,REAL st b1 = f1 (#) f2 holds
b1 is Lipschitzian
proof end;
end;

theorem :: FCONT_1:36
for X, X1, Z, Z1 being set
for f1, f2 being PartFunc of REAL,REAL st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian & f1 | Z is bounded & f2 | Z1 is bounded holds
(f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) is Lipschitzian
proof end;

registration
let f be Lipschitzian PartFunc of REAL,REAL;
let p be Real;
cluster p (#) f -> Lipschitzian for PartFunc of REAL,REAL;
coherence
for b1 being PartFunc of REAL,REAL st b1 = p (#) f holds
b1 is Lipschitzian
proof end;
end;

theorem :: FCONT_1:37
for X being set
for p being Real
for f being PartFunc of REAL,REAL st f | X is Lipschitzian & X c= dom f holds
(p (#) f) | X is Lipschitzian
proof end;

registration
let f be Lipschitzian PartFunc of REAL,REAL;
cluster |.f.| -> Lipschitzian for PartFunc of REAL,REAL;
coherence
for b1 being PartFunc of REAL,REAL st b1 = abs f holds
b1 is Lipschitzian
proof end;
end;

theorem :: FCONT_1:38
for X being set
for f being PartFunc of REAL,REAL st f | X is Lipschitzian holds
( - (f | X) is Lipschitzian & (abs f) | X is Lipschitzian )
proof end;

registration
coherence
for b1 being PartFunc of REAL,REAL st b1 is V8() holds
b1 is Lipschitzian
proof end;
end;

registration
let Y be Subset of REAL;
cluster id Y -> Lipschitzian for PartFunc of REAL,REAL;
coherence
for b1 being PartFunc of REAL,REAL st b1 = id Y holds
b1 is Lipschitzian
proof end;
end;

registration
coherence
for b1 being PartFunc of REAL,REAL st b1 is Lipschitzian holds
b1 is continuous
proof end;
end;

theorem :: FCONT_1:39
for f being PartFunc of REAL,REAL st ex r being Real st rng f = {r} holds
f is continuous
proof end;

theorem :: FCONT_1:40
for f being PartFunc of REAL,REAL st ( for x0 being Real st x0 in dom f holds
f . x0 = x0 ) holds
f is continuous
proof end;

theorem Th41: :: FCONT_1:41
for X being set
for r, p being Real
for f being PartFunc of REAL,REAL st ( for x0 being Real st x0 in X holds
f . x0 = (r * x0) + p ) holds
f | X is continuous
proof end;

theorem Th42: :: FCONT_1:42
for f being PartFunc of REAL,REAL st ( for x0 being Real st x0 in dom f holds
f . x0 = x0 ^2 ) holds
f | (dom f) is continuous
proof end;

theorem :: FCONT_1:43
for X being set
for f being PartFunc of REAL,REAL st X c= dom f & ( for x0 being Real st x0 in X holds
f . x0 = x0 ^2 ) holds
f | X is continuous
proof end;

theorem Th44: :: FCONT_1:44
for f being PartFunc of REAL,REAL st ( for x0 being Real st x0 in dom f holds
f . x0 = |.x0.| ) holds
f is continuous
proof end;

theorem :: FCONT_1:45
for X being set
for f being PartFunc of REAL,REAL st ( for x0 being Real st x0 in X holds
f . x0 = |.x0.| ) holds
f | X is continuous
proof end;

theorem Th46: :: FCONT_1:46
for X being set
for f being PartFunc of REAL,REAL st f | X is monotone & ex p, g being Real st
( p <= g & f .: X = [.p,g.] ) holds
f | X is continuous
proof end;

theorem :: FCONT_1:47
for g, p being Real
for f being one-to-one PartFunc of REAL,REAL st p <= g & [.p,g.] c= dom f & ( f | [.p,g.] is increasing or f | [.p,g.] is decreasing ) holds
((f | [.p,g.]) ") | (f .: [.p,g.]) is continuous
proof end;

:: from
definition
let a, b be Real;
func AffineMap (a,b) -> Function of REAL,REAL means :Def4: :: FCONT_1:def 4
for x being Real holds it . x = (a * x) + b;
existence
ex b1 being Function of REAL,REAL st
for x being Real holds b1 . x = (a * x) + b
proof end;
uniqueness
for b1, b2 being Function of REAL,REAL st ( for x being Real holds b1 . x = (a * x) + b ) & ( for x being Real holds b2 . x = (a * x) + b ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines AffineMap FCONT_1:def 4 :
for a, b being Real
for b3 being Function of REAL,REAL holds
( b3 = AffineMap (a,b) iff for x being Real holds b3 . x = (a * x) + b );

registration
let a, b be Real;
cluster AffineMap (a,b) -> continuous ;
coherence
AffineMap (a,b) is continuous
proof end;
end;

registration
existence
ex b1 being Function of REAL,REAL st b1 is continuous
proof end;
end;

theorem Th48: :: FCONT_1:48
for a, b being Real holds (AffineMap (a,b)) . 0 = b
proof end;

theorem Th49: :: FCONT_1:49
for a, b being Real holds (AffineMap (a,b)) . 1 = a + b
proof end;

theorem Th50: :: FCONT_1:50
for a, b being Real st a <> 0 holds
AffineMap (a,b) is one-to-one
proof end;

theorem :: FCONT_1:51
for a, b, x, y being Real st a > 0 & x < y holds
(AffineMap (a,b)) . x < (AffineMap (a,b)) . y
proof end;

theorem :: FCONT_1:52
for a, b, x, y being Real st a < 0 & x < y holds
(AffineMap (a,b)) . x > (AffineMap (a,b)) . y
proof end;

theorem Th53: :: FCONT_1:53
for a, b, x, y being Real st a >= 0 & x <= y holds
(AffineMap (a,b)) . x <= (AffineMap (a,b)) . y
proof end;

theorem :: FCONT_1:54
for a, b, x, y being Real st a <= 0 & x <= y holds
(AffineMap (a,b)) . x >= (AffineMap (a,b)) . y
proof end;

theorem Th55: :: FCONT_1:55
for a, b being Real st a <> 0 holds
rng (AffineMap (a,b)) = REAL
proof end;

theorem :: FCONT_1:56
for a, b being Real st a <> 0 holds
(AffineMap (a,b)) " = AffineMap ((a "),(- (b / a)))
proof end;

theorem :: FCONT_1:57
for a, b being Real st a > 0 holds
(AffineMap (a,b)) .: [.0,1.] = [.b,(a + b).]
proof end;