:: ALI2 semantic presentation

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

proof end;

end;

:: deftheorem Def1 defines contraction ALI2:def 1 :

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;