:: by Alicia de la Cruz

::

:: Received July 17, 1991

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

:: deftheorem Def1 defines contraction ALI2:def 1 :

for M being non empty MetrSpace

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 dist ((f . x),(f . y)) <= L * (dist (x,y)) ) ) );

for M being non empty MetrSpace

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 dist ((f . x),(f . y)) <= L * (dist (x,y)) ) ) );

registration

let M be non empty MetrSpace;

for b_{1} being Function of M,M st b_{1} is constant holds

b_{1} is contraction

end;
cluster Function-like constant V21( the carrier of M, the carrier of M) -> contraction for Element of K10(K11( the carrier of M, the carrier of M));

coherence for b

b

proof end;

registration

let M be non empty MetrSpace;

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

end;
cluster non empty Relation-like the carrier of M -defined the carrier of M -valued Function-like constant V17( the carrier of M) V21( the carrier of M, the carrier of M) for Element of K10(K11( the carrier of M, the carrier of M));

existence ex b

proof end;

:: Banach fixed-point theorem

theorem :: ALI2:1

for M being non empty MetrSpace

for f being Contraction of M st TopSpaceMetr M is compact holds

ex c being Point of M st

( f . c = c & ( for x being Point of M st f . x = x holds

x = c ) )

for f being Contraction of M st TopSpaceMetr M is compact holds

ex c being Point of M st

( f . c = c & ( for x being Point of M st f . x = x holds

x = c ) )

proof end;