:: NFCONT_2 semantic presentation

definition

let c₁ be set ;
let c₂, c₃ be RealNormSpace;
let c₄ be PartFunc of c₂,c₃;
pred c₄ is_uniformly_continuous_on c₁ means :Def1: :: NFCONT_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 Point of a₂ st b₃ in a₁ & b₄ in a₁ & ||.(b₃ - b₄).|| < b₂ holds
||.((a₄ /. b₃) - (a₄ /. b₄)).|| < b₁ ) ) ) );

end;

:: deftheorem Def1 defines is_uniformly_continuous_on NFCONT_2:def 1 :

definition

let c₁ be set ;
let c₂ be RealNormSpace;
let c₃ be PartFunc of the carrier of c₂, REAL ;
pred c₃ is_uniformly_continuous_on c₁ means :Def2: :: NFCONT_2:def 2
( a₁ c= dom a₃ & ( for b₁ being Real st 0 < b₁ holds
ex b₂ being Real st
( 0 < b₂ & ( for b₃, b₄ being Point of a₂ st b₃ in a₁ & b₄ in a₁ & ||.(b₃ - b₄).|| < b₂ holds
abs ((a₃ /. b₃) - (a₃ /. b₄)) < b₁ ) ) ) );

end;

:: deftheorem Def2 defines is_uniformly_continuous_on NFCONT_2:def 2 :

theorem Th1: :: NFCONT_2:1

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

proof end;

theorem Th2: :: NFCONT_2:2

for b₁, b₂ being set
for b₃, b₄ being RealNormSpace
for b₅, b₆ being PartFunc of b₃,b₄ 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 Th3: :: NFCONT_2:3

for b₁, b₂ being set
for b₃, b₄ being RealNormSpace
for b₅, b₆ being PartFunc of b₃,b₄ 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: :: NFCONT_2:4

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

proof end;

theorem Th5: :: NFCONT_2:5

for b₁ being set
for b₂, b₃ being RealNormSpace
for b₄ being PartFunc of b₂,b₃ st b₄ is_uniformly_continuous_on b₁ holds
- b₄ is_uniformly_continuous_on b₁

proof end;

theorem Th6: :: NFCONT_2:6

for b₁ being set
for b₂, b₃ being RealNormSpace
for b₄ being PartFunc of b₂,b₃ st b₄ is_uniformly_continuous_on b₁ holds
||.b₄.|| is_uniformly_continuous_on b₁

proof end;

theorem Th7: :: NFCONT_2:7

for b₁ being set
for b₂, b₃ being RealNormSpace
for b₄ being PartFunc of b₂,b₃ st b₄ is_uniformly_continuous_on b₁ holds
b₄ is_continuous_on b₁

proof end;

theorem Th8: :: NFCONT_2:8

for b₁ being set
for b₂ being RealNormSpace
for b₃ being PartFunc of the carrier of b₂, REAL st b₃ is_uniformly_continuous_on b₁ holds
b₃ is_continuous_on b₁

proof end;

theorem Th9: :: NFCONT_2:9

for b₁ being set
for b₂, b₃ being RealNormSpace
for b₄ being PartFunc of b₂,b₃ st b₄ is_Lipschitzian_on b₁ holds
b₄ is_uniformly_continuous_on b₁

proof end;

theorem Th10: :: NFCONT_2:10

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

proof end;

theorem Th11: :: NFCONT_2:11

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

proof end;

theorem Th12: :: NFCONT_2:12

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

proof end;

theorem Th13: :: NFCONT_2:13

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

proof end;

definition

let c₁ be RealBanachSpace;
mode contraction of c₁ -> Function of the carrier of a₁,the carrier of a₁ means :Def3: :: NFCONT_2:def 3
ex b₁ being Real st
( 0 < b₁ & b₁ < 1 & ( for b₂, b₃ being Point of a₁ holds ||.((a₂ . b₂) - (a₂ . b₃)).|| <= b₁ * ||.(b₂ - b₃).|| ) );
existence

proof end;

end;

:: deftheorem Def3 defines contraction NFCONT_2:def 3 :

Lemma9: ( ( for b₁ being RealNormSpace
for b₂, b₃ being Point of b₁ holds
( ||.(b₂ - b₃).|| = 0 iff b₂ = b₃ ) ) & ( for b₁ being RealNormSpace
for b₂, b₃ being Point of b₁ holds
( ||.(b₂ - b₃).|| <> 0 iff b₂ <> b₃ ) ) & ( for b₁ being RealNormSpace
for b₂, b₃ being Point of b₁ holds
( ||.(b₂ - b₃).|| > 0 iff b₂ <> b₃ ) ) & ( for b₁ being RealNormSpace
for b₂, b₃ being Point of b₁ holds ||.(b₂ - b₃).|| = ||.(b₃ - b₂).|| ) & ( for b₁ being RealNormSpace
for b₂, b₃, b₄ being Point of b₁
for b₅ being Real st b₅ > 0 & ||.(b₂ - b₄).|| < b₅ / 2 & ||.(b₄ - b₃).|| < b₅ / 2 holds
||.(b₂ - b₃).|| < b₅ ) & ( for b₁ being RealNormSpace
for b₂, b₃, b₄ being Point of b₁
for b₅ being Real st b₅ > 0 & ||.(b₂ - b₄).|| < b₅ / 2 & ||.(b₃ - b₄).|| < b₅ / 2 holds
||.(b₂ - b₃).|| < b₅ ) & ( for b₁ being RealNormSpace
for b₂ being Point of b₁ st ( for b₃ being Real st b₃ > 0 holds
||.b₂.|| < b₃ ) holds
b₂ = 0. b₁ ) & ( for b₁ being RealNormSpace
for b₂, b₃ being Point of b₁ st ( for b₄ being Real st b₄ > 0 holds
||.(b₂ - b₃).|| < b₄ ) holds
b₂ = b₃ ) )

proof end;

Lemma10: for b₁, b₂, b₃ being real number st 0 < b₁ & b₁ < 1 & 0 < b₃ holds
ex b₄ being Nat st abs (b₂ * (b₁ to_power b₄)) < b₃

proof end;

theorem Th14: :: NFCONT_2:14

for b₁ being RealBanachSpace
for b₂ being Function of b₁,b₁ st b₂ is contraction of b₁ holds
ex b₃ being Point of b₁ st
( b₂ . b₃ = b₃ & ( for b₄ being Point of b₁ st b₂ . b₄ = b₄ holds
b₃ = b₄ ) )

proof end;

theorem Th15: :: NFCONT_2:15

for b₁ being RealBanachSpace
for b₂ being Function of b₁,b₁ st ex b₃ being Nat st iter b₂,b₃ is contraction of b₁ holds
ex b₃ being Point of b₁ st
( b₂ . b₃ = b₃ & ( for b₄ being Point of b₁ st b₂ . b₄ = b₄ holds
b₃ = b₄ ) )

proof end;

theorem Th16: :: NFCONT_2:16

for b₁, b₂, b₃ being real number st 0 < b₁ & b₁ < 1 & 0 < b₃ holds
ex b₄ being Nat st abs (b₂ * (b₁ to_power b₄)) < b₃ by Lemma10;