Journal of Formalized Mathematics
Volume 3, 1991
University of Bialystok
Copyright (c) 1991 Association of Mizar Users

### Fix Point Theorem for Compact Spaces

by
Alicia de la Cruz

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;
```