:: Fix Point Theorem for Compact Spaces
:: by Alicia de la Cruz
::
:: Received July 17, 1991
:: Copyright (c) 1991 Association of Mizar Users
definition
let
M
be non
empty
MetrSpace
;
mode
contraction
of
M
->
Function
of
M
,
M
means
:
Def1
:
:: 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
)
) );
existence
ex
b
1
being
Function
of
M
,
M
ex
L
being
Real
st
(
0
<
L
&
L
<
1 & ( for
x
,
y
being
Point
of
M
holds
dist
(
b
1
.
x
)
,
(
b
1
.
y
)
<=
L
*
(
dist
x
,
y
)
) )
proof
end;
end;
::
deftheorem
Def1
defines
contraction
ALI2:def 1 :
for
M
being non
empty
MetrSpace
for
b
2
being
Function
of
M
,
M
holds
(
b
2
is
contraction
of
M
iff ex
L
being
Real
st
(
0
<
L
&
L
<
1 & ( for
x
,
y
being
Point
of
M
holds
dist
(
b
2
.
x
)
,
(
b
2
.
y
)
<=
L
*
(
dist
x
,
y
)
) ) );
theorem
:: ALI2:1
canceled;
theorem
:: ALI2:2
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;