The abstract of the Mizar article:

Fix Point Theorem for Compact Spaces

by

Alicia de la Cruz

Received July 17, 1991

MML identifier: ALI2

[ Mizar article, MML identifier index ]

environ

 vocabulary METRIC_1, FINSET_1, BOOLE, ZFMISC_1, FUNCT_1, PRE_TOPC, FUNCOP_1,
      RELAT_1, ARYTM_3, PCOMPS_1, COMPTS_1, SETFAM_1, POWER, SUBSET_1, ARYTM_1,
      SEQ_1, SEQ_2, ORDINAL2, SEQM_3, ALI2, HAHNBAN;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XREAL_0, FINSET_1, SETFAM_1,
      METRIC_1, RELAT_1, FUNCT_2, STRUCT_0, PRE_TOPC, POWER, FUNCOP_1,
      COMPTS_1, PCOMPS_1, TOPS_2, SEQ_1, SEQ_2, SEQM_3, REAL_1, NAT_1;
 constructors FINSET_1, POWER, FUNCOP_1, COMPTS_1, PCOMPS_1, TOPS_2, SEQ_2,
      SEQM_3, REAL_1, NAT_1, PARTFUN1, MEMBERED;
 clusters STRUCT_0, PCOMPS_1, FUNCOP_1, XREAL_0, SEQ_1, METRIC_1, MEMBERED,
      ZFMISC_1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin
  reserve M for non empty MetrSpace;

theorem :: ALI2:1
for F being set st F is finite & F <> {} & F is c=-linear
 ex m being set st m in F & for C being set st C in F holds m c= C;

definition let M be non empty MetrSpace;
  mode contraction of M -> Function of the carrier of M, the carrier of 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;

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;