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

environ

 vocabularies METRIC_1, FINSET_1, BOOLE, FUNCT_1, PRE_TOPC, FUNCOP_1, ARYTM_3,
      PCOMPS_1, COMPTS_1, SETFAM_1, POWER, SUBSET_1, ARYTM_1, SEQ_1, SEQ_2,
      ORDINAL2, ALI2, HAHNBAN, ARYTM;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, FINSET_1, SETFAM_1,
      METRIC_1, FUNCT_2, STRUCT_0, PRE_TOPC, POWER, FUNCOP_1, COMPTS_1,
      PCOMPS_1, TOPS_2, VALUED_1, SEQ_1, SEQ_2, XXREAL_0, REAL_1, NAT_1;
 constructors SETFAM_1, FUNCOP_1, FINSET_1, XXREAL_0, REAL_1, NAT_1, SEQ_2,
      POWER, TOPS_2, COMPTS_1, PCOMPS_1, SEQ_1, VALUED_1, PARTFUN1;
 registrations XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, MEMBERED,
      SEQM_3, STRUCT_0, METRIC_1, PCOMPS_1, VALUED_1, FUNCT_2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

reserve M for non empty MetrSpace;

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

canceled;

theorem :: ALI2:2
  for f being contraction of M st TopSpaceMetr(M) is compact
  ex c being Point of M st f.c =c &            :: exists a fix point
  for x being Point of M st f.x=x holds x=c;