:: Fix Point Theorem for Compact Spaces
:: by Alicia de la Cruz
::
:: Received July 17, 1991
:: Copyright (c) 1991 Association of Mizar Users

begin

definition

let M be non empty MetrSpace;
mode contraction of M -> Function of M,M means :Def1: :: ALI2:def 1
ex L being Real st
( 0 < L & L < 1 & ( for x, y being Point of M holds dist ((it . x),(it . y)) <= L * (dist (x,y)) ) );
existence
ex b₁ being Function of M,M ex L being Real st
( 0 < L & L < 1 & ( for x, y being Point of M holds dist ((b₁ . x),(b₁ . y)) <= L * (dist (x,y)) ) )

proof end;

end;

:: deftheorem Def1 defines contraction ALI2:def 1 :
for M being non empty MetrSpace
for b₂ being Function of M,M holds
( b₂ is contraction of M iff ex L being Real st
( 0 < L & L < 1 & ( for x, y being Point of M holds dist ((b₂ . x),(b₂ . y)) <= L * (dist (x,y)) ) ) );

theorem :: ALI2:1

canceled;

theorem :: ALI2:2

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;