:: Fix Point Theorem for Compact Spaces
:: by Alicia de la Cruz
::
:: Copyright (c) 1991-2021 Association of Mizar Users

definition
let M be non empty MetrSpace;
let f be Function of M,M;
attr f is contraction means :Def1: :: ALI2:def 1
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)) ) );
end;

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

registration
let M be non empty MetrSpace;
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 b1 being Function of M,M st b1 is constant holds
b1 is contraction
proof end;
end;

registration
let M be non empty MetrSpace;
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 b1 being Function of M,M st b1 is constant
proof end;
end;

definition
let M be non empty MetrSpace;
mode Contraction of M is contraction Function of M,M;
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 ) )
proof end;