:: FCONT_2 semantic presentation

definition

let f be PartFunc of REAL , REAL ;
let X be set ;
pred f is_uniformly_continuous_on X means :Def1: :: FCONT_2:def 1
( X c= dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in X & x2 in X & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < r ) ) ) );

end;

:: deftheorem Def1 defines is_uniformly_continuous_on FCONT_2:def 1 :

theorem :: FCONT_2:1

canceled;

theorem Th2: :: FCONT_2:2

for X, X1 being set
for f being PartFunc of REAL , REAL st f is_uniformly_continuous_on X & X1 c= X holds
f is_uniformly_continuous_on X1

proof end;

theorem :: FCONT_2:3

for X, X1 being set
for f1, f2 being PartFunc of REAL , REAL st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds
f1 + f2 is_uniformly_continuous_on X /\ X1

proof end;

theorem :: FCONT_2:4

for X, X1 being set
for f1, f2 being PartFunc of REAL , REAL st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds
f1 - f2 is_uniformly_continuous_on X /\ X1

proof end;

theorem Th5: :: FCONT_2:5

for X being set
for p being Real
for f being PartFunc of REAL , REAL st f is_uniformly_continuous_on X holds
p (#) f is_uniformly_continuous_on X

proof end;

theorem :: FCONT_2:6

for X being set
for f being PartFunc of REAL , REAL st f is_uniformly_continuous_on X holds
- f is_uniformly_continuous_on X

proof end;

theorem :: FCONT_2:7

for X being set
for f being PartFunc of REAL , REAL st f is_uniformly_continuous_on X holds
abs f is_uniformly_continuous_on X

proof end;

theorem :: FCONT_2:8

for X, X1, Z, Z1 being set
for f1, f2 being PartFunc of REAL , REAL st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 & f1 is_bounded_on Z & f2 is_bounded_on Z1 holds
f1 (#) f2 is_uniformly_continuous_on ((X /\ Z) /\ X1) /\ Z1

proof end;

theorem Th9: :: FCONT_2:9

for X being set
for f being PartFunc of REAL , REAL st f is_uniformly_continuous_on X holds
f is_continuous_on X

proof end;

theorem Th10: :: FCONT_2:10

for X being set
for f being PartFunc of REAL , REAL st f is_Lipschitzian_on X holds
f is_uniformly_continuous_on X

proof end;

theorem Th11: :: FCONT_2:11

for f being PartFunc of REAL , REAL
for Y being Subset of REAL st Y is compact & f is_continuous_on Y holds
f is_uniformly_continuous_on Y

proof end;

theorem :: FCONT_2:12

canceled;

theorem :: FCONT_2:13

for Y being Subset of REAL
for f being PartFunc of REAL , REAL st Y c= dom f & Y is compact & f is_uniformly_continuous_on Y holds
f .: Y is compact

proof end;

theorem :: FCONT_2:14

for f being PartFunc of REAL , REAL
for Y being Subset of REAL st Y <> {} & Y c= dom f & Y is compact & f is_uniformly_continuous_on Y 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;

theorem :: FCONT_2:15

for X being set
for f being PartFunc of REAL , REAL st X c= dom f & f is_constant_on X holds
f is_uniformly_continuous_on X

proof end;

theorem Th16: :: FCONT_2:16

for p, g being Real
for f being PartFunc of REAL , REAL st p <= g & f is_continuous_on [.p,g.] 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 Th17: :: FCONT_2:17

for p, g being Real
for f being PartFunc of REAL , REAL st p <= g & f is_continuous_on [.p,g.] 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 Th18: :: FCONT_2:18

for p, g being Real
for f being PartFunc of REAL , REAL st f is one-to-one & p <= g & f is_continuous_on [.p,g.] & not f is_increasing_on [.p,g.] holds
f is_decreasing_on [.p,g.]

proof end;

theorem :: FCONT_2:19

for p, g being Real
for f being PartFunc of REAL , REAL st f is one-to-one & p <= g & f is_continuous_on [.p,g.] & 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;

theorem Th20: :: FCONT_2:20

for p, g being Real
for f being PartFunc of REAL , REAL st p <= g & f is_continuous_on [.p,g.] holds
f .: [.p,g.] = [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).]

proof end;

theorem :: FCONT_2:21

for p, g being Real
for f being one-to-one PartFunc of REAL , REAL st p <= g & f is_continuous_on [.p,g.] holds
f " is_continuous_on [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).]

proof end;