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


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

:: deftheorem 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 & ( for x1, x2 being Real st x1 in dom f & x2 in dom f & |.(x1 - x2).| < s holds
|.((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 & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & |.(x1 - x2).| < s holds
|.((f . x1) - (f . x2)).| < r ) ) )
proof end;

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

theorem :: FCONT_2:3
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 uniformly_continuous & f2 | X1 is uniformly_continuous holds
(f1 + f2) | (X /\ X1) is uniformly_continuous
proof end;

theorem :: FCONT_2:4
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 uniformly_continuous & f2 | X1 is uniformly_continuous holds
(f1 - f2) | (X /\ X1) is uniformly_continuous
proof end;

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 & f | X is uniformly_continuous holds
(p (#) f) | X is uniformly_continuous
proof end;

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

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

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

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

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

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

theorem :: FCONT_2:12
for Y being Subset of REAL
for f being PartFunc of REAL,REAL st Y c= dom f & Y is compact & 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 <> {} & Y c= dom f & Y is compact & f | Y is uniformly_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) ) by Th9, FCONT_1:31;

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

theorem Th15: :: FCONT_2:15
for g, p being Real
for f being PartFunc of REAL,REAL st p <= g & [.p,g.] c= dom f & 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.] & r = f . s )
proof end;

theorem Th16: :: FCONT_2:16
for g, p being Real
for f being PartFunc of REAL,REAL st p <= g & [.p,g.] c= dom f & 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.] & r = f . s )
proof end;

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

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

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

theorem :: FCONT_2:20
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 continuous holds
(f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous
proof end;