:: by Jaros{\l}aw Kotowicz and Konrad Raczkowski

::

:: Received June 18, 1990

:: Copyright (c) 1990-2019 Association of Mizar Users

:: 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 ) ) );

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 ) ) )

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

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

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

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

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

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

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

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

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

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

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

theorem :: FCONT_2:13

theorem :: FCONT_2:14

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 )

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 )

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

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 )

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;

:: 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.])).]

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

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;