:: ALI2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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 b1 being Function of M,M ex L being Real st
( 0 < L & L < 1 & ( for x, y being Point of M holds dist (b1 . x),(b1 . y) <= L * (dist x,y) ) )
proof end;
end;

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

theorem :: ALI2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ALI2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;