:: by Noboru Endou

::

:: Received October 6, 2004

:: Copyright (c) 2004-2019 Association of Mizar Users

:: deftheorem 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 ) ) ) ) );

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 ) ) ) ) );

definition
end;

:: deftheorem 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 ) ) ) ) );

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 ) ) ) ) );

definition
end;

:: deftheorem 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 ) ) ) ) );

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 ) ) ) ) );

definition
end;

:: deftheorem 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 ) ) ) ) );

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 ) ) ) ) );

definition
end;

:: deftheorem 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

|.((f /. x1) - (f /. x2)).| < r ) ) ) ) );

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

|.((f /. x1) - (f /. x2)).| < r ) ) ) ) );

definition
end;

:: deftheorem 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 ) ) ) ) );

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: :: NCFCONT2:1

for X, X1 being set

for CNS1, CNS2 being ComplexNormSpace

for f being PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X & X1 c= X holds

f is_uniformly_continuous_on X1

for CNS1, CNS2 being ComplexNormSpace

for f being PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X & X1 c= X holds

f is_uniformly_continuous_on X1

proof end;

theorem Th2: :: NCFCONT2:2

for X, X1 being set

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X & X1 c= X holds

f is_uniformly_continuous_on X1

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X & X1 c= X holds

f is_uniformly_continuous_on X1

proof end;

theorem Th3: :: NCFCONT2:3

for X, X1 being set

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X & X1 c= X holds

f is_uniformly_continuous_on X1

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X & X1 c= X holds

f is_uniformly_continuous_on X1

proof end;

theorem :: NCFCONT2:4

for X, X1 being set

for CNS1, CNS2 being ComplexNormSpace

for f1, f2 being PartFunc of CNS1,CNS2 st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds

f1 + f2 is_uniformly_continuous_on X /\ X1

for CNS1, CNS2 being ComplexNormSpace

for f1, f2 being PartFunc of CNS1,CNS2 st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds

f1 + f2 is_uniformly_continuous_on X /\ X1

proof end;

theorem :: NCFCONT2:5

for X, X1 being set

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f1, f2 being PartFunc of CNS,RNS st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds

f1 + f2 is_uniformly_continuous_on X /\ X1

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f1, f2 being PartFunc of CNS,RNS st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds

f1 + f2 is_uniformly_continuous_on X /\ X1

proof end;

theorem :: NCFCONT2:6

for X, X1 being set

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f1, f2 being PartFunc of RNS,CNS st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds

f1 + f2 is_uniformly_continuous_on X /\ X1

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f1, f2 being PartFunc of RNS,CNS st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds

f1 + f2 is_uniformly_continuous_on X /\ X1

proof end;

theorem :: NCFCONT2:7

for X, X1 being set

for CNS1, CNS2 being ComplexNormSpace

for f1, f2 being PartFunc of CNS1,CNS2 st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds

f1 - f2 is_uniformly_continuous_on X /\ X1

for CNS1, CNS2 being ComplexNormSpace

for f1, f2 being PartFunc of CNS1,CNS2 st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds

f1 - f2 is_uniformly_continuous_on X /\ X1

proof end;

theorem :: NCFCONT2:8

for X, X1 being set

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f1, f2 being PartFunc of CNS,RNS st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds

f1 - f2 is_uniformly_continuous_on X /\ X1

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f1, f2 being PartFunc of CNS,RNS st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds

f1 - f2 is_uniformly_continuous_on X /\ X1

proof end;

theorem :: NCFCONT2:9

for X, X1 being set

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f1, f2 being PartFunc of RNS,CNS st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds

f1 - f2 is_uniformly_continuous_on X /\ X1

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f1, f2 being PartFunc of RNS,CNS st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds

f1 - f2 is_uniformly_continuous_on X /\ X1

proof end;

theorem Th10: :: NCFCONT2:10

for X being set

for z being Complex

for CNS1, CNS2 being ComplexNormSpace

for f being PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X holds

z (#) f is_uniformly_continuous_on X

for z being Complex

for CNS1, CNS2 being ComplexNormSpace

for f being PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X holds

z (#) f is_uniformly_continuous_on X

proof end;

theorem Th11: :: NCFCONT2:11

for X being set

for r being Real

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X holds

r (#) f is_uniformly_continuous_on X

for r being Real

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X holds

r (#) f is_uniformly_continuous_on X

proof end;

theorem Th12: :: NCFCONT2:12

for X being set

for z being Complex

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds

z (#) f is_uniformly_continuous_on X

for z being Complex

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds

z (#) f is_uniformly_continuous_on X

proof end;

theorem :: NCFCONT2:13

for X being set

for CNS1, CNS2 being ComplexNormSpace

for f being PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X holds

- f is_uniformly_continuous_on X

for CNS1, CNS2 being ComplexNormSpace

for f being PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X holds

- f is_uniformly_continuous_on X

proof end;

theorem :: NCFCONT2:14

for X being set

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X holds

- f is_uniformly_continuous_on X

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X holds

- f is_uniformly_continuous_on X

proof end;

theorem :: NCFCONT2:15

for X being set

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds

- f is_uniformly_continuous_on X

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds

- f is_uniformly_continuous_on X

proof end;

theorem :: NCFCONT2:16

for X being set

for CNS1, CNS2 being ComplexNormSpace

for f being PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X holds

||.f.|| is_uniformly_continuous_on X

for CNS1, CNS2 being ComplexNormSpace

for f being PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X holds

||.f.|| is_uniformly_continuous_on X

proof end;

theorem :: NCFCONT2:17

for X being set

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X holds

||.f.|| is_uniformly_continuous_on X

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X holds

||.f.|| is_uniformly_continuous_on X

proof end;

theorem :: NCFCONT2:18

for X being set

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds

||.f.|| is_uniformly_continuous_on X

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds

||.f.|| is_uniformly_continuous_on X

proof end;

theorem Th19: :: NCFCONT2:19

for X being set

for CNS1, CNS2 being ComplexNormSpace

for f being PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X holds

f is_continuous_on X

for CNS1, CNS2 being ComplexNormSpace

for f being PartFunc of CNS1,CNS2 st f is_uniformly_continuous_on X holds

f is_continuous_on X

proof end;

theorem Th20: :: NCFCONT2:20

for X being set

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X holds

f is_continuous_on X

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f being PartFunc of CNS,RNS st f is_uniformly_continuous_on X holds

f is_continuous_on X

proof end;

theorem Th21: :: NCFCONT2:21

for X being set

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds

f is_continuous_on X

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f being PartFunc of RNS,CNS st f is_uniformly_continuous_on X holds

f is_continuous_on X

proof end;

theorem :: NCFCONT2:22

for X being set

for CNS being ComplexNormSpace

for f being PartFunc of the carrier of CNS,COMPLEX st f is_uniformly_continuous_on X holds

f is_continuous_on X

for CNS being ComplexNormSpace

for f being PartFunc of the carrier of CNS,COMPLEX st f is_uniformly_continuous_on X holds

f is_continuous_on X

proof end;

theorem Th23: :: NCFCONT2:23

for X being set

for CNS being ComplexNormSpace

for f being PartFunc of the carrier of CNS,REAL st f is_uniformly_continuous_on X holds

f is_continuous_on X

for CNS being ComplexNormSpace

for f being PartFunc of the carrier of CNS,REAL st f is_uniformly_continuous_on X holds

f is_continuous_on X

proof end;

theorem :: NCFCONT2:24

for X being set

for RNS being RealNormSpace

for f being PartFunc of the carrier of RNS,COMPLEX st f is_uniformly_continuous_on X holds

f is_continuous_on X

for RNS being RealNormSpace

for f being PartFunc of the carrier of RNS,COMPLEX st f is_uniformly_continuous_on X holds

f is_continuous_on X

proof end;

theorem Th25: :: NCFCONT2:25

for X being set

for CNS1, CNS2 being ComplexNormSpace

for f being PartFunc of CNS1,CNS2 st f is_Lipschitzian_on X holds

f is_uniformly_continuous_on X

for CNS1, CNS2 being ComplexNormSpace

for f being PartFunc of CNS1,CNS2 st f is_Lipschitzian_on X holds

f is_uniformly_continuous_on X

proof end;

theorem Th26: :: NCFCONT2:26

for X being set

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f being PartFunc of CNS,RNS st f is_Lipschitzian_on X holds

f is_uniformly_continuous_on X

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f being PartFunc of CNS,RNS st f is_Lipschitzian_on X holds

f is_uniformly_continuous_on X

proof end;

theorem Th27: :: NCFCONT2:27

for X being set

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f being PartFunc of RNS,CNS st f is_Lipschitzian_on X holds

f is_uniformly_continuous_on X

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f being PartFunc of RNS,CNS st f is_Lipschitzian_on X holds

f is_uniformly_continuous_on X

proof end;

theorem :: NCFCONT2:28

for CNS1, CNS2 being ComplexNormSpace

for f being PartFunc of CNS1,CNS2

for Y being Subset of CNS1 st Y is compact & f is_continuous_on Y holds

f is_uniformly_continuous_on Y

for f being PartFunc of CNS1,CNS2

for Y being Subset of CNS1 st Y is compact & f is_continuous_on Y holds

f is_uniformly_continuous_on Y

proof end;

theorem :: NCFCONT2:29

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f being PartFunc of CNS,RNS

for Y being Subset of CNS st Y is compact & f is_continuous_on Y holds

f is_uniformly_continuous_on Y

for CNS being ComplexNormSpace

for f being PartFunc of CNS,RNS

for Y being Subset of CNS st Y is compact & f is_continuous_on Y holds

f is_uniformly_continuous_on Y

proof end;

theorem :: NCFCONT2:30

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f being PartFunc of RNS,CNS

for Y being Subset of RNS st Y is compact & f is_continuous_on Y holds

f is_uniformly_continuous_on Y

for CNS being ComplexNormSpace

for f being PartFunc of RNS,CNS

for Y being Subset of RNS st Y is compact & f is_continuous_on Y holds

f is_uniformly_continuous_on Y

proof end;

theorem :: NCFCONT2:31

for CNS1, CNS2 being ComplexNormSpace

for f being PartFunc of CNS1,CNS2

for Y being Subset of CNS1 st Y c= dom f & Y is compact & f is_uniformly_continuous_on Y holds

f .: Y is compact by Th19, NCFCONT1:83;

for f being PartFunc of CNS1,CNS2

for Y being Subset of CNS1 st Y c= dom f & Y is compact & f is_uniformly_continuous_on Y holds

f .: Y is compact by Th19, NCFCONT1:83;

theorem :: NCFCONT2:32

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f being PartFunc of CNS,RNS

for Y being Subset of CNS st Y c= dom f & Y is compact & f is_uniformly_continuous_on Y holds

f .: Y is compact by Th20, NCFCONT1:84;

for CNS being ComplexNormSpace

for f being PartFunc of CNS,RNS

for Y being Subset of CNS st Y c= dom f & Y is compact & f is_uniformly_continuous_on Y holds

f .: Y is compact by Th20, NCFCONT1:84;

theorem :: NCFCONT2:33

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f being PartFunc of RNS,CNS

for Y being Subset of RNS st Y c= dom f & Y is compact & f is_uniformly_continuous_on Y holds

f .: Y is compact by Th21, NCFCONT1:85;

for CNS being ComplexNormSpace

for f being PartFunc of RNS,CNS

for Y being Subset of RNS st Y c= dom f & Y is compact & f is_uniformly_continuous_on Y holds

f .: Y is compact by Th21, NCFCONT1:85;

theorem :: NCFCONT2:34

for CNS being ComplexNormSpace

for f being PartFunc of the carrier of CNS,REAL

for Y being Subset of CNS st Y <> {} & Y c= dom f & Y is compact & f is_uniformly_continuous_on Y holds

ex x1, x2 being Point of CNS st

( x1 in Y & x2 in Y & f /. x1 = upper_bound (f .: Y) & f /. x2 = lower_bound (f .: Y) ) by Th23, NCFCONT1:96;

for f being PartFunc of the carrier of CNS,REAL

for Y being Subset of CNS st Y <> {} & Y c= dom f & Y is compact & f is_uniformly_continuous_on Y holds

ex x1, x2 being Point of CNS st

( x1 in Y & x2 in Y & f /. x1 = upper_bound (f .: Y) & f /. x2 = lower_bound (f .: Y) ) by Th23, NCFCONT1:96;

theorem :: NCFCONT2:35

for X being set

for CNS1, CNS2 being ComplexNormSpace

for f being PartFunc of CNS1,CNS2 st X c= dom f & f | X is constant holds

f is_uniformly_continuous_on X by Th25, NCFCONT1:112;

for CNS1, CNS2 being ComplexNormSpace

for f being PartFunc of CNS1,CNS2 st X c= dom f & f | X is constant holds

f is_uniformly_continuous_on X by Th25, NCFCONT1:112;

theorem :: NCFCONT2:36

for X being set

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f being PartFunc of CNS,RNS st X c= dom f & f | X is constant holds

f is_uniformly_continuous_on X by Th26, NCFCONT1:113;

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f being PartFunc of CNS,RNS st X c= dom f & f | X is constant holds

f is_uniformly_continuous_on X by Th26, NCFCONT1:113;

theorem :: NCFCONT2:37

for X being set

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f being PartFunc of RNS,CNS st X c= dom f & f | X is constant holds

f is_uniformly_continuous_on X by Th27, NCFCONT1:114;

for RNS being RealNormSpace

for CNS being ComplexNormSpace

for f being PartFunc of RNS,CNS st X c= dom f & f | X is constant holds

f is_uniformly_continuous_on X by Th27, NCFCONT1:114;

:: deftheorem Def7 defines contraction NCFCONT2:def 7 :

for M being non empty CNORMSTR

for f being Function of M,M holds

( f is contraction iff ex L being Real st

( 0 < L & L < 1 & ( for x, y being Point of M holds ||.((f . x) - (f . y)).|| <= L * ||.(x - y).|| ) ) );

for M being non empty CNORMSTR

for f being Function of M,M holds

( f is contraction iff ex L being Real st

( 0 < L & L < 1 & ( for x, y being Point of M holds ||.((f . x) - (f . y)).|| <= L * ||.(x - y).|| ) ) );

registration

let M be ComplexBanachSpace;

ex b_{1} being Function of M,M st b_{1} is contraction

end;
cluster Relation-like the carrier of M -defined the carrier of M -valued non empty Function-like total quasi_total contraction for Element of K16(K17( the carrier of M, the carrier of M));

existence ex b

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

theorem Th40: :: NCFCONT2:40

for X being ComplexBanachSpace

for f being Function of X,X st f is Contraction of X holds

ex xp being Point of X st

( f . xp = xp & ( for x being Point of X st f . x = x holds

xp = x ) )

for f being Function of X,X st f is Contraction of X holds

ex xp being Point of X st

( f . xp = xp & ( for x being Point of X st f . x = x holds

xp = x ) )

proof end;

theorem :: NCFCONT2:41

for X being ComplexBanachSpace

for f being Function of X,X st ex n0 being Element of NAT st iter (f,n0) is Contraction of X holds

ex xp being Point of X st

( f . xp = xp & ( for x being Point of X st f . x = x holds

xp = x ) )

for f being Function of X,X st ex n0 being Element of NAT st iter (f,n0) is Contraction of X holds

ex xp being Point of X st

( f . xp = xp & ( for x being Point of X st f . x = x holds

xp = x ) )

proof end;