:: FCONT_2 semantic presentation

definition

let c₁ be PartFunc of REAL , REAL ;
let c₂ be set ;
pred c₁ is_uniformly_continuous_on c₂ means :Def1: :: FCONT_2:def 1
( a₂ c= dom a₁ & ( for b₁ being Real st 0 < b₁ holds
ex b₂ being Real st
( 0 < b₂ & ( for b₃, b₄ being Real st b₃ in a₂ & b₄ in a₂ & abs (b₃ - b₄) < b₂ holds
abs ((a₁ . b₃) - (a₁ . b₄)) < b₁ ) ) ) );

end;

:: deftheorem Def1 defines is_uniformly_continuous_on FCONT_2:def 1 :

theorem Th1: :: FCONT_2:1

canceled;

theorem Th2: :: FCONT_2:2

for b₁, b₂ being set
for b₃ being PartFunc of REAL , REAL st b₃ is_uniformly_continuous_on b₁ & b₂ c= b₁ holds
b₃ is_uniformly_continuous_on b₂

proof end;

theorem Th3: :: FCONT_2:3

for b₁, b₂ being set
for b₃, b₄ being PartFunc of REAL , REAL st b₃ is_uniformly_continuous_on b₁ & b₄ is_uniformly_continuous_on b₂ holds
b₃ + b₄ is_uniformly_continuous_on b₁ /\ b₂

proof end;

theorem Th4: :: FCONT_2:4

for b₁, b₂ being set
for b₃, b₄ being PartFunc of REAL , REAL st b₃ is_uniformly_continuous_on b₁ & b₄ is_uniformly_continuous_on b₂ holds
b₃ - b₄ is_uniformly_continuous_on b₁ /\ b₂

proof end;

theorem Th5: :: FCONT_2:5

for b₁ being set
for b₂ being Real
for b₃ being PartFunc of REAL , REAL st b₃ is_uniformly_continuous_on b₁ holds
b₂ (#) b₃ is_uniformly_continuous_on b₁

proof end;

theorem Th6: :: FCONT_2:6

for b₁ being set
for b₂ being PartFunc of REAL , REAL st b₂ is_uniformly_continuous_on b₁ holds
- b₂ is_uniformly_continuous_on b₁

proof end;

theorem Th7: :: FCONT_2:7

for b₁ being set
for b₂ being PartFunc of REAL , REAL st b₂ is_uniformly_continuous_on b₁ holds
abs b₂ is_uniformly_continuous_on b₁

proof end;

theorem Th8: :: FCONT_2:8

for b₁, b₂, b₃, b₄ being set
for b₅, b₆ being PartFunc of REAL , REAL st b₅ is_uniformly_continuous_on b₁ & b₆ is_uniformly_continuous_on b₂ & b₅ is_bounded_on b₃ & b₆ is_bounded_on b₄ holds
b₅ (#) b₆ is_uniformly_continuous_on ((b₁ /\ b₃) /\ b₂) /\ b₄

proof end;

theorem Th9: :: FCONT_2:9

for b₁ being set
for b₂ being PartFunc of REAL , REAL st b₂ is_uniformly_continuous_on b₁ holds
b₂ is_continuous_on b₁

proof end;

theorem Th10: :: FCONT_2:10

for b₁ being set
for b₂ being PartFunc of REAL , REAL st b₂ is_Lipschitzian_on b₁ holds
b₂ is_uniformly_continuous_on b₁

proof end;

theorem Th11: :: FCONT_2:11

for b₁ being PartFunc of REAL , REAL
for b₂ being Subset of REAL st b₂ is compact & b₁ is_continuous_on b₂ holds
b₁ is_uniformly_continuous_on b₂

proof end;

theorem Th12: :: FCONT_2:12

canceled;

theorem Th13: :: FCONT_2:13

for b₁ being Subset of REAL
for b₂ being PartFunc of REAL , REAL st b₁ c= dom b₂ & b₁ is compact & b₂ is_uniformly_continuous_on b₁ holds
b₂ .: b₁ is compact

proof end;

theorem Th14: :: FCONT_2:14

for b₁ being PartFunc of REAL , REAL
for b₂ being Subset of REAL st b₂ <> {} & b₂ c= dom b₁ & b₂ is compact & b₁ is_uniformly_continuous_on b₂ holds
ex b₃, b₄ being Real st
( b₃ in b₂ & b₄ in b₂ & b₁ . b₃ = upper_bound (b₁ .: b₂) & b₁ . b₄ = lower_bound (b₁ .: b₂) )

proof end;

theorem Th15: :: FCONT_2:15

for b₁ being set
for b₂ being PartFunc of REAL , REAL st b₁ c= dom b₂ & b₂ is_constant_on b₁ holds
b₂ is_uniformly_continuous_on b₁

proof end;

theorem Th16: :: FCONT_2:16

for b₁, b₂ being Real
for b₃ being PartFunc of REAL , REAL st b₁ <= b₂ & b₃ is_continuous_on [.b₁,b₂.] holds
for b₄ being Real st b₄ in [.(b₃ . b₁),(b₃ . b₂).] \/ [.(b₃ . b₂),(b₃ . b₁).] holds
ex b₅ being Real st
( b₅ in [.b₁,b₂.] & b₄ = b₃ . b₅ )

proof end;

theorem Th17: :: FCONT_2:17

for b₁, b₂ being Real
for b₃ being PartFunc of REAL , REAL st b₁ <= b₂ & b₃ is_continuous_on [.b₁,b₂.] holds
for b₄ being Real st b₄ in [.(lower_bound (b₃ .: [.b₁,b₂.])),(upper_bound (b₃ .: [.b₁,b₂.])).] holds
ex b₅ being Real st
( b₅ in [.b₁,b₂.] & b₄ = b₃ . b₅ )

proof end;

theorem Th18: :: FCONT_2:18

for b₁, b₂ being Real
for b₃ being PartFunc of REAL , REAL st b₃ is one-to-one & b₁ <= b₂ & b₃ is_continuous_on [.b₁,b₂.] & not b₃ is_increasing_on [.b₁,b₂.] holds
b₃ is_decreasing_on [.b₁,b₂.]

proof end;

theorem Th19: :: FCONT_2:19

for b₁, b₂ being Real
for b₃ being PartFunc of REAL , REAL st b₃ is one-to-one & b₁ <= b₂ & b₃ is_continuous_on [.b₁,b₂.] & not ( lower_bound (b₃ .: [.b₁,b₂.]) = b₃ . b₁ & upper_bound (b₃ .: [.b₁,b₂.]) = b₃ . b₂ ) holds
( lower_bound (b₃ .: [.b₁,b₂.]) = b₃ . b₂ & upper_bound (b₃ .: [.b₁,b₂.]) = b₃ . b₁ )

proof end;

theorem Th20: :: FCONT_2:20

for b₁, b₂ being Real
for b₃ being PartFunc of REAL , REAL st b₁ <= b₂ & b₃ is_continuous_on [.b₁,b₂.] holds
b₃ .: [.b₁,b₂.] = [.(lower_bound (b₃ .: [.b₁,b₂.])),(upper_bound (b₃ .: [.b₁,b₂.])).]

proof end;

theorem Th21: :: FCONT_2:21

for b₁, b₂ being Real
for b₃ being one-to-one PartFunc of REAL , REAL st b₁ <= b₂ & b₃ is_continuous_on [.b₁,b₂.] holds
b₃ " is_continuous_on [.(lower_bound (b₃ .: [.b₁,b₂.])),(upper_bound (b₃ .: [.b₁,b₂.])).]

proof end;