:: Fix Point Theorem for Compact Spaces
:: by Alicia de la Cruz
::
:: Received July 17, 1991
:: Copyright (c) 1991-2021 Association of Mizar Users
definition
let
M
be non
empty
MetrSpace
;
let
f
be
Function
of
M
,
M
;
attr
f
is
contraction
means
:
Def1
:
:: 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;
::
deftheorem
Def1
defines
contraction
ALI2:def 1 :
for
M
being non
empty
MetrSpace
for
f
being
Function
of
M
,
M
holds
(
f
is
contraction
iff 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
)
)
) ) );
registration
let
M
be non
empty
MetrSpace
;
cluster
Function-like
constant
V21
( the
carrier
of
M
, the
carrier
of
M
)
->
contraction
for
Element
of
K10
(
K11
( the
carrier
of
M
, the
carrier
of
M
));
coherence
for
b
1
being
Function
of
M
,
M
st
b
1
is
constant
holds
b
1
is
contraction
proof
end;
end;
registration
let
M
be non
empty
MetrSpace
;
cluster
non
empty
Relation-like
the
carrier
of
M
-defined
the
carrier
of
M
-valued
Function-like
constant
V17
( the
carrier
of
M
)
V21
( the
carrier
of
M
, the
carrier
of
M
) for
Element
of
K10
(
K11
( the
carrier
of
M
, the
carrier
of
M
));
existence
ex
b
1
being
Function
of
M
,
M
st
b
1
is
constant
proof
end;
end;
definition
let
M
be non
empty
MetrSpace
;
mode
Contraction of
M
is
contraction
Function
of
M
,
M
;
end;
::
Banach fixed-point theorem
theorem
:: ALI2:1
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;