begin
:: deftheorem Def1 defines is_uniformly_continuous_on NCFCONT2:def 1 :
for X being set
for CNS1, CNS2 being ComplexNormSpace
for f being PartFunc of CNS1,CNS2 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 CNS1 st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) ) ) ) );
:: deftheorem Def2 defines is_uniformly_continuous_on NCFCONT2:def 2 :
for X being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of CNS,RNS 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 CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) ) ) ) );
:: deftheorem Def3 defines is_uniformly_continuous_on NCFCONT2:def 3 :
for X being set
for RNS being RealNormSpace
for CNS being ComplexNormSpace
for f being PartFunc of RNS,CNS 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 RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) ) ) ) );
:: deftheorem Def4 defines is_uniformly_continuous_on NCFCONT2:def 4 :
for X being set
for CNS being ComplexNormSpace
for f being PartFunc of the carrier of CNS,COMPLEX 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 CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
|.((f /. x1) - (f /. x2)).| < r ) ) ) ) );
:: deftheorem Def5 defines is_uniformly_continuous_on NCFCONT2:def 5 :
for X being set
for CNS being ComplexNormSpace
for f being PartFunc of the carrier of CNS,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 CNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
abs ((f /. x1) - (f /. x2)) < r ) ) ) ) );
:: deftheorem Def6 defines is_uniformly_continuous_on NCFCONT2:def 6 :
for X being set
for RNS being RealNormSpace
for f being PartFunc of the carrier of RNS,COMPLEX 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 RNS st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
|.((f /. x1) - (f /. x2)).| < r ) ) ) ) );
theorem Th1:
theorem Th2:
theorem Th3:
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th10:
theorem Th11:
theorem Th12:
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th19:
theorem Th20:
theorem Th21:
theorem
theorem Th23:
theorem
theorem Th25:
theorem Th26:
theorem Th27:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
begin
:: deftheorem Def7 defines contraction NCFCONT2:def 7 :
for M being ComplexBanachSpace
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).|| ) ) );
theorem
theorem
Lm1:
for X being ComplexNormSpace
for x, y, z being Point of X
for e being Real st ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 holds
||.(x - y).|| < e
Lm2:
for X being ComplexNormSpace
for x, y, z being Point of X
for e being Real st ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 holds
||.(x - y).|| < e
Lm3:
for X being ComplexNormSpace
for x being Point of X st ( for e being Real st e > 0 holds
||.x.|| < e ) holds
x = 0. X
Lm4:
for X being ComplexNormSpace
for x, y being Point of X st ( for e being Real st e > 0 holds
||.(x - y).|| < e ) holds
x = y
theorem Th40:
theorem