:: NCFCONT2 semantic presentation

definition

let c₁ be set ;
let c₂, c₃ be ComplexNormSpace;
let c₄ be PartFunc of c₂,c₃;
pred c₄ is_uniformly_continuous_on c₁ means :Def1: :: NCFCONT2: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 NCFCONT2:def 1 :

definition

let c₁ be set ;
let c₂ be RealNormSpace;
let c₃ be ComplexNormSpace;
let c₄ be PartFunc of c₃,c₂;
pred c₄ is_uniformly_continuous_on c₁ means :Def2: :: NCFCONT2: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
||.((a₄ /. b₃) - (a₄ /. b₄)).|| < b₁ ) ) ) );

end;

:: deftheorem Def2 defines is_uniformly_continuous_on NCFCONT2:def 2 :

definition

let c₁ be set ;
let c₂ be RealNormSpace;
let c₃ be ComplexNormSpace;
let c₄ be PartFunc of c₂,c₃;
pred c₄ is_uniformly_continuous_on c₁ means :Def3: :: NCFCONT2:def 3
( 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 Def3 defines is_uniformly_continuous_on NCFCONT2:def 3 :

definition

let c₁ be set ;
let c₂ be ComplexNormSpace;
let c₃ be PartFunc of the carrier of c₂, COMPLEX ;
pred c₃ is_uniformly_continuous_on c₁ means :Def4: :: NCFCONT2:def 4
( 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 Def4 defines is_uniformly_continuous_on NCFCONT2:def 4 :

definition

let c₁ be set ;
let c₂ be ComplexNormSpace;
let c₃ be PartFunc of the carrier of c₂, REAL ;
pred c₃ is_uniformly_continuous_on c₁ means :Def5: :: NCFCONT2:def 5
( 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 Def5 defines is_uniformly_continuous_on NCFCONT2:def 5 :

definition

let c₁ be set ;
let c₂ be RealNormSpace;
let c₃ be PartFunc of the carrier of c₂, COMPLEX ;
pred c₃ is_uniformly_continuous_on c₁ means :Def6: :: NCFCONT2:def 6
( 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 Def6 defines is_uniformly_continuous_on NCFCONT2:def 6 :

theorem Th1: :: NCFCONT2:1

for b₁, b₂ being set
for b₃, b₄ being ComplexNormSpace
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: :: NCFCONT2:2

for b₁, b₂ being set
for b₃ being RealNormSpace
for b₄ being ComplexNormSpace
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 Th3: :: NCFCONT2:3

for b₁, b₂ being set
for b₃ being RealNormSpace
for b₄ being ComplexNormSpace
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 Th4: :: NCFCONT2:4

for b₁, b₂ being set
for b₃, b₄ being ComplexNormSpace
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 Th5: :: NCFCONT2:5

for b₁, b₂ being set
for b₃ being RealNormSpace
for b₄ being ComplexNormSpace
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 Th6: :: NCFCONT2:6

for b₁, b₂ being set
for b₃ being RealNormSpace
for b₄ being ComplexNormSpace
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 Th7: :: NCFCONT2:7

for b₁, b₂ being set
for b₃, b₄ being ComplexNormSpace
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 Th8: :: NCFCONT2:8

proof end;

theorem Th9: :: NCFCONT2:9

proof end;

theorem Th10: :: NCFCONT2:10

for b₁ being set
for b₂ being Complex
for b₃, b₄ being ComplexNormSpace
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 Th11: :: NCFCONT2:11

for b₁ being set
for b₂ being Real
for b₃ being RealNormSpace
for b₄ being ComplexNormSpace
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 Th12: :: NCFCONT2:12

for b₁ being set
for b₂ being Complex
for b₃ being RealNormSpace
for b₄ being ComplexNormSpace
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 Th13: :: NCFCONT2:13

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

proof end;

theorem Th14: :: NCFCONT2:14

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

proof end;

theorem Th15: :: NCFCONT2:15

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

proof end;

theorem Th16: :: NCFCONT2:16

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

proof end;

theorem Th17: :: NCFCONT2:17

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

proof end;

theorem Th18: :: NCFCONT2:18

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

proof end;

theorem Th19: :: NCFCONT2:19

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

proof end;

theorem Th20: :: NCFCONT2:20

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

proof end;

theorem Th21: :: NCFCONT2:21

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

proof end;

theorem Th22: :: NCFCONT2:22

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

proof end;

theorem Th23: :: NCFCONT2:23

for b₁ being set
for b₂ being ComplexNormSpace
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 Th24: :: NCFCONT2:24

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

proof end;

theorem Th25: :: NCFCONT2:25

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

proof end;

theorem Th26: :: NCFCONT2:26

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

proof end;

theorem Th27: :: NCFCONT2:27

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

proof end;

theorem Th28: :: NCFCONT2:28

for b₁, b₂ being ComplexNormSpace
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 Th29: :: NCFCONT2:29

for b₁ being RealNormSpace
for b₂ being ComplexNormSpace
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 Th30: :: NCFCONT2:30

for b₁ being RealNormSpace
for b₂ being ComplexNormSpace
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 Th31: :: NCFCONT2:31

for b₁, b₂ being ComplexNormSpace
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 Th32: :: NCFCONT2:32

for b₁ being RealNormSpace
for b₂ being ComplexNormSpace
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 Th33: :: NCFCONT2:33

for b₁ being RealNormSpace
for b₂ being ComplexNormSpace
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 Th34: :: NCFCONT2:34

for b₁ being ComplexNormSpace
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 Th35: :: NCFCONT2:35

for b₁ being set
for b₂, b₃ being ComplexNormSpace
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;

theorem Th36: :: NCFCONT2:36

for b₁ being set
for b₂ being RealNormSpace
for b₃ being ComplexNormSpace
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;

theorem Th37: :: NCFCONT2:37

for b₁ being set
for b₂ being RealNormSpace
for b₃ being ComplexNormSpace
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 ComplexBanachSpace;
mode contraction of c₁ -> Function of the carrier of a₁,the carrier of a₁ means :Def7: :: NCFCONT2:def 7
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 Def7 defines contraction NCFCONT2:def 7 :

theorem Th38: :: NCFCONT2:38

for b₁ being ComplexNormSpace
for b₂, b₃ being Point of b₁ holds
( ||.(b₂ - b₃).|| > 0 iff b₂ <> b₃ )

proof end;

theorem Th39: :: NCFCONT2:39

for b₁ being ComplexNormSpace
for b₂, b₃ being Point of b₁ holds ||.(b₂ - b₃).|| = ||.(b₃ - b₂).||

proof end;

Lemma21: for b₁ being ComplexNormSpace
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₅

proof end;

Lemma22: for b₁ being ComplexNormSpace
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₅

proof end;

Lemma23: for b₁ being ComplexNormSpace
for b₂ being Point of b₁ st ( for b₃ being Real st b₃ > 0 holds
||.b₂.|| < b₃ ) holds
b₂ = 0. b₁

proof end;

Lemma24: for b₁ being ComplexNormSpace
for b₂, b₃ being Point of b₁ st ( for b₄ being Real st b₄ > 0 holds
||.(b₂ - b₃).|| < b₄ ) holds
b₂ = b₃

proof end;

Lemma25: 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 NFCONT_2:16;

theorem Th40: :: NCFCONT2:40

for b₁ being ComplexBanachSpace
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 Th41: :: NCFCONT2:41

for b₁ being ComplexBanachSpace
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;