:: Fix Point Theorem for Compact Spaces
::  by Alicia de la Cruz
::
:: Received July 17, 1991
:: Copyright (c) 1991-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies 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;
 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, BINOP_2,
      RVSUM_1, COMSEQ_2;
 registrations SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, MEMBERED, STRUCT_0,
      METRIC_1, PCOMPS_1, VALUED_1, FUNCT_2, FUNCOP_1, SEQ_4, XREAL_0;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

reserve M for non empty MetrSpace;

definition
  let M be non empty MetrSpace;
  let f be Function of M, M;
  attr f is contraction means
:: 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;

registration
  let M be non empty MetrSpace;
  cluster contraction for Function of M, M;
end;

definition
 let M be non empty MetrSpace;
 mode Contraction of M is contraction Function of M, M;
end;

::$N Banach Fix Point Theorem for Compact Spaces
theorem :: ALI2:1
  for f being Contraction of M st TopSpaceMetr(M) is compact ex c being
  Point of M st f.c =c & for x being Point of M st f.x=x holds x=c;