begin
:: deftheorem Def1 defines is_uniformly_continuous_on NFCONT_2:def 1 :
for X being set
for S, T being RealNormSpace
for f being PartFunc of S,T holds
( f is_uniformly_continuous_on X iff ( X c= dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) ) ) ) );
:: deftheorem Def2 defines is_uniformly_continuous_on NFCONT_2:def 2 :
for X being set
for S being RealNormSpace
for f being PartFunc of the carrier of S,REAL holds
( f is_uniformly_continuous_on X iff ( X c= dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
abs ((f /. x1) - (f /. x2)) < r ) ) ) ) );
theorem Th1:
theorem
theorem
theorem Th4:
theorem
theorem
theorem Th7:
theorem Th8:
theorem Th9:
theorem
theorem
theorem
theorem
begin
:: deftheorem Def3 defines contraction NFCONT_2:def 3 :
for M being RealBanachSpace
for b2 being Function of the carrier of M, the carrier of M holds
( b2 is contraction of M iff ex L being Real st
( 0 < L & L < 1 & ( for x, y being Point of M holds ||.((b2 . x) - (b2 . y)).|| <= L * ||.(x - y).|| ) ) );
Lm1:
( ( for X being RealNormSpace
for x, y being Point of X holds
( ||.(x - y).|| = 0 iff x = y ) ) & ( for X being RealNormSpace
for x, y being Point of X holds
( ||.(x - y).|| <> 0 iff x <> y ) ) & ( for X being RealNormSpace
for x, y being Point of X holds
( ||.(x - y).|| > 0 iff x <> y ) ) & ( for X being RealNormSpace
for x, y being Point of X holds ||.(x - y).|| = ||.(y - x).|| ) & ( for X being RealNormSpace
for x, y, z being Point of X
for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 holds
||.(x - y).|| < e ) & ( for X being RealNormSpace
for x, y, z being Point of X
for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 holds
||.(x - y).|| < e ) & ( for X being RealNormSpace
for x being Point of X st ( for e being Real st e > 0 holds
||.x.|| < e ) holds
x = 0. X ) & ( for X being RealNormSpace
for x, y being Point of X st ( for e being Real st e > 0 holds
||.(x - y).|| < e ) holds
x = y ) )
Lm2:
for K, L, e being real number st 0 < K & K < 1 & 0 < e holds
ex n being Element of NAT st abs (L * (K to_power n)) < e
theorem Th14:
theorem
theorem