:: Real Function Uniform Continuity
:: by Jaros{\l}aw Kotowicz and Konrad Raczkowski
::
:: Received June 18, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

definition
let f be PartFunc of REAL,REAL;
attrf is uniformly_continuous  means :Def1: :: FCONT_2:def 1
 for r being Real st 0 < r holds
ex s being Real st
( 0 < s &amp; ( for x1, x2 being Real st x1 in dom f &amp; x2 in dom f &amp; abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < r ) );
end;

:: deftheorem Def1 defines uniformly_continuous FCONT_2:def_1_:_
 for f being PartFunc of REAL,REAL holds
( f is uniformly_continuous iff for r being Real st 0 < r holds
ex s being Real st
( 0 < s &amp; ( for x1, x2 being Real st x1 in dom f &amp; x2 in dom f &amp; abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < r ) ) );

theorem Th1: :: FCONT_2:1
for X being set
for f being PartFunc of REAL,REAL holds
( f | X is uniformly_continuous iff for r being Real st 0 < r holds
ex s being Real st
( 0 < s &amp; ( for x1, x2 being Real st x1 in dom (f | X) &amp; x2 in dom (f | X) &amp; abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < r ) ) )
proofend;

theorem Th2: :: FCONT_2:2
for X, X1 being set
for f being PartFunc of REAL,REAL st f | X is uniformly_continuous &amp; X1 c= X holds
f | X1 is uniformly_continuous
proofend;

theorem :: FCONT_2:3
for X, X1 being set
for f1, f2 being PartFunc of REAL,REAL st X c= dom f1 &amp; X1 c= dom f2 &amp; f1 | X is uniformly_continuous &amp; f2 | X1 is uniformly_continuous holds
(f1 + f2) | (X /\ X1) is uniformly_continuous
proofend;

theorem :: FCONT_2:4
for X, X1 being set
for f1, f2 being PartFunc of REAL,REAL st X c= dom f1 &amp; X1 c= dom f2 &amp; f1 | X is uniformly_continuous &amp; f2 | X1 is uniformly_continuous holds
(f1 - f2) | (X /\ X1) is uniformly_continuous
proofend;

theorem Th5: :: FCONT_2:5
for X being set
for p being Real
for f being PartFunc of REAL,REAL st X c= dom f &amp; f | X is uniformly_continuous holds
(p (#) f) | X is uniformly_continuous
proofend;

theorem :: FCONT_2:6
for X being set
for f being PartFunc of REAL,REAL st X c= dom f &amp; f | X is uniformly_continuous holds
(- f) | X is uniformly_continuous
proofend;

theorem :: FCONT_2:7
for X being set
for f being PartFunc of REAL,REAL st f | X is uniformly_continuous holds
(abs f) | X is uniformly_continuous
proofend;

theorem :: FCONT_2:8
for X, X1, Z, Z1 being set
for f1, f2 being PartFunc of REAL,REAL st X c= dom f1 &amp; X1 c= dom f2 &amp; f1 | X is uniformly_continuous &amp; f2 | X1 is uniformly_continuous &amp; f1 | Z is bounded &amp; f2 | Z1 is bounded holds
(f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) is uniformly_continuous
proofend;

theorem Th9: :: FCONT_2:9
for X being set
for f being PartFunc of REAL,REAL st X c= dom f &amp; f | X is uniformly_continuous holds
f | X is continuous
proofend;

theorem Th10: :: FCONT_2:10
for X being set
for f being PartFunc of REAL,REAL st f | X is Lipschitzian holds
f | X is uniformly_continuous
proofend;

theorem Th11: :: FCONT_2:11
for f being PartFunc of REAL,REAL
for Y being Subset of REAL st Y c= dom f &amp; Y is compact &amp; f | Y is continuous holds
f | Y is uniformly_continuous
proofend;

theorem :: FCONT_2:12
for Y being Subset of REAL
for f being PartFunc of REAL,REAL st Y c= dom f &amp; Y is compact &amp; f | Y is uniformly_continuous holds
f .: Y is compact by Th9, FCONT_1:29;

theorem :: FCONT_2:13
for f being PartFunc of REAL,REAL
for Y being Subset of REAL st Y <> {} &amp; Y c= dom f &amp; Y is compact &amp; f | Y is uniformly_continuous holds
ex x1, x2 being Real st
( x1 in Y &amp; x2 in Y &amp; f . x1 = upper_bound (f .: Y) &amp; f . x2 = lower_bound (f .: Y) )
proofend;

theorem :: FCONT_2:14
for X being set
for f being PartFunc of REAL,REAL st X c= dom f &amp; f | X is V8() holds
f | X is uniformly_continuous by Th10;

theorem Th15: :: FCONT_2:15
for p, g being Real
for f being PartFunc of REAL,REAL st p <= g &amp; [.p,g.] c= dom f &amp; f | [.p,g.] is continuous holds
for r being Real st r in [.(f . p),(f . g).] \/ [.(f . g),(f . p).] holds
ex s being Real st
( s in [.p,g.] &amp; r = f . s )
proofend;

theorem Th16: :: FCONT_2:16
for p, g being Real
for f being PartFunc of REAL,REAL st p <= g &amp; [.p,g.] c= dom f &amp; f | [.p,g.] is continuous holds
for r being Real st r in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] holds
ex s being Real st
( s in [.p,g.] &amp; r = f . s )
proofend;

theorem Th17: :: FCONT_2:17
for p, g being Real
for f being PartFunc of REAL,REAL st f is one-to-one &amp; [.p,g.] c= dom f &amp; p <= g &amp; f | [.p,g.] is continuous &amp; not f | [.p,g.] is increasing holds
f | [.p,g.] is decreasing
proofend;

theorem :: FCONT_2:18
for p, g being Real
for f being PartFunc of REAL,REAL st f is one-to-one &amp; p <= g &amp; [.p,g.] c= dom f &amp; f | [.p,g.] is continuous &amp; not ( lower_bound (f .: [.p,g.]) = f . p &amp; upper_bound (f .: [.p,g.]) = f . g ) holds
( lower_bound (f .: [.p,g.]) = f . g &amp; upper_bound (f .: [.p,g.]) = f . p )
proofend;

:: [WP: ] Darboux_Theorem
theorem Th19: :: FCONT_2:19
for p, g being Real
for f being PartFunc of REAL,REAL st p <= g &amp; [.p,g.] c= dom f &amp; f | [.p,g.] is continuous holds
f .: [.p,g.] = [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).]
proofend;

theorem :: FCONT_2:20
for p, g being Real
for f being one-to-one PartFunc of REAL,REAL st p <= g &amp; [.p,g.] c= dom f &amp; f | [.p,g.] is continuous holds
(f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous
proofend;