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

environ

vocabularies HIDDEN, NUMBERS, XBOOLE_0, METRIC_1, FUNCT_1, REAL_1, CARD_1, ARYTM_3, PRE_TOPC, XXREAL_0, RELAT_1, STRUCT_0, FUNCOP_1, PCOMPS_1, RCOMP_1, SUBSET_1, POWER, SETFAM_1, TARSKI, ARYTM_1, FINSET_1, ORDINAL1, SEQ_1, VALUED_1, ORDINAL2, SEQ_2, ALI2, NAT_1, ASYMPT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, FINSET_1, SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, STRUCT_0, METRIC_1, PRE_TOPC, POWER, COMPTS_1, PCOMPS_1, TOPS_2, VALUED_1, SEQ_1, SEQ_2, XXREAL_0, REAL_1, NAT_1;
definitions TARSKI, TOPS_2, ORDINAL1, XBOOLE_0, FINSET_1;
theorems METRIC_1, SUBSET_1, PCOMPS_1, COMPTS_1, POWER, SEQ_2, SEQ_4, SERIES_1, SETFAM_1, SEQ_1, PRE_TOPC, TOPS_1, FINSET_1, XREAL_1, XXREAL_0, XBOOLE_0, XREAL_0, FUNCT_1, FUNCT_2;
schemes SUBSET_1, SEQ_1, DOMAIN_1, NAT_1;
registrations SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, MEMBERED, STRUCT_0, METRIC_1, PCOMPS_1, VALUED_1, FUNCT_2, XREAL_0, SEQ_1, SEQ_2, RELSET_1, FUNCOP_1;
constructors HIDDEN, SETFAM_1, FUNCOP_1, FINSET_1, XXREAL_0, REAL_1, NAT_1, SEQ_2, POWER, TOPS_2, COMPTS_1, PCOMPS_1, VALUED_1, PARTFUN1, BINOP_2, RVSUM_1, COMSEQ_2, SEQ_1, RELSET_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities XBOOLE_0, SUBSET_1, STRUCT_0;
expansions ;


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;

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