let M be 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 ) )
let f be contraction of M; ( TopSpaceMetr M is compact implies ex c being Point of M st
( f . c = c & ( for x being Point of M st f . x = x holds
x = c ) ) )
consider x0 being Point of M;
set a = dist x0,(f . x0);
consider L being Real such that
A1:
0 < L
and
A2:
L < 1
and
A3:
for x, y being Point of M holds dist (f . x),(f . y) <= L * (dist x,y)
by Def1;
assume A4:
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 ) )
now deffunc H1(
Element of
NAT )
-> Element of
REAL =
L to_power ($1 + 1);
defpred S1[
set ]
means ex
n being
Element of
NAT st $1
= { x where x is Point of M : dist x,(f . x) <= (dist x0,(f . x0)) * (L to_power n) } ;
assume
dist x0,
(f . x0) <> 0
;
ex c being Point of M st dist c,(f . c) = 0 consider F being
Subset-Family of
(TopSpaceMetr M) such that A5:
for
B being
Subset of
(TopSpaceMetr M) holds
(
B in F iff
S1[
B] )
from SUBSET_1:sch 3();
defpred S2[
Point of
M]
means dist $1,
(f . $1) <= (dist x0,(f . x0)) * (L to_power (0 + 1));
A6:
F is
closed
proof
let B be
Subset of
(TopSpaceMetr M);
TOPS_2:def 2 ( not B in F or B is closed )
A7:
TopSpaceMetr M = TopStruct(# the
carrier of
M,
(Family_open_set M) #)
by PCOMPS_1:def 6;
then reconsider V =
B ` as
Subset of
M ;
assume
B in F
;
B is closed
then consider n being
Element of
NAT such that A8:
B = { x where x is Point of M : dist x,(f . x) <= (dist x0,(f . x0)) * (L to_power n) }
by A5;
for
x being
Point of
M st
x in V holds
ex
r being
Real st
(
r > 0 &
Ball x,
r c= V )
proof
let x be
Point of
M;
( x in V implies ex r being Real st
( r > 0 & Ball x,r c= V ) )
assume
x in V
;
ex r being Real st
( r > 0 & Ball x,r c= V )
then
not
x in B
by XBOOLE_0:def 5;
then
dist x,
(f . x) > (dist x0,(f . x0)) * (L to_power n)
by A8;
then A9:
(dist x,(f . x)) - ((dist x0,(f . x0)) * (L to_power n)) > 0
by XREAL_1:52;
take r =
((dist x,(f . x)) - ((dist x0,(f . x0)) * (L to_power n))) / 2;
( r > 0 & Ball x,r c= V )
thus
r > 0
by A9, XREAL_1:217;
Ball x,r c= V
let z be
set ;
TARSKI:def 3 ( not z in Ball x,r or z in V )
assume A10:
z in Ball x,
r
;
z in V
then reconsider y =
z as
Point of
M ;
dist x,
y < r
by A10, METRIC_1:12;
then
2
* (dist x,y) < 2
* r
by XREAL_1:70;
then A11:
(dist y,(f . y)) + (2 * (dist x,y)) < (dist y,(f . y)) + (2 * r)
by XREAL_1:8;
(dist x,y) + (dist y,(f . y)) >= dist x,
(f . y)
by METRIC_1:4;
then A12:
((dist x,y) + (dist y,(f . y))) + (dist (f . y),(f . x)) >= (dist x,(f . y)) + (dist (f . y),(f . x))
by XREAL_1:8;
(
dist (f . y),
(f . x) <= L * (dist y,x) &
L * (dist y,x) <= dist y,
x )
by A2, A3, METRIC_1:5, XREAL_1:155;
then
dist (f . y),
(f . x) <= dist y,
x
by XXREAL_0:2;
then
(dist (f . y),(f . x)) + (dist y,x) <= (dist y,x) + (dist y,x)
by XREAL_1:8;
then A13:
(dist y,(f . y)) + ((dist y,x) + (dist (f . y),(f . x))) <= (dist y,(f . y)) + (2 * (dist y,x))
by XREAL_1:9;
(dist x,(f . y)) + (dist (f . y),(f . x)) >= dist x,
(f . x)
by METRIC_1:4;
then
((dist y,(f . y)) + (dist x,y)) + (dist (f . y),(f . x)) >= dist x,
(f . x)
by A12, XXREAL_0:2;
then
(dist y,(f . y)) + (2 * (dist x,y)) >= dist x,
(f . x)
by A13, XXREAL_0:2;
then
(
(dist x,(f . x)) - (2 * r) = (dist x0,(f . x0)) * (L to_power n) &
(dist y,(f . y)) + (2 * r) > dist x,
(f . x) )
by A11, XXREAL_0:2;
then
for
x being
Point of
M holds
( not
y = x or not
dist x,
(f . x) <= (dist x0,(f . x0)) * (L to_power n) )
by XREAL_1:21;
then
not
y in B
by A8;
hence
z in V
by A7, SUBSET_1:50;
verum
end;
then
B ` in Family_open_set M
by PCOMPS_1:def 5;
then
B ` is
open
by A7, PRE_TOPC:def 5;
hence
B is
closed
by TOPS_1:29;
verum
end; A14:
TopSpaceMetr M = TopStruct(# the
carrier of
M,
(Family_open_set M) #)
by PCOMPS_1:def 6;
A15:
{ x where x is Point of M : S2[x] } is
Subset of
M
from DOMAIN_1:sch 7();
F is
centered
proof
thus
F <> {}
by A5, A14, A15;
FINSET_1:def 3 for b1 being set holds
( b1 = {} or not b1 c= F or not b1 is finite or not meet b1 = {} )
defpred S3[
Element of
NAT ]
means { x where x is Point of M : dist x,(f . x) <= (dist x0,(f . x0)) * (L to_power $1) } <> {} ;
let G be
set ;
( G = {} or not G c= F or not G is finite or not meet G = {} )
assume that A16:
G <> {}
and A17:
G c= F
and A18:
G is
finite
;
not meet G = {}
G is
c=-linear
proof
let B,
C be
set ;
ORDINAL1:def 9 ( not B in G or not C in G or B,C are_c=-comparable )
assume that A19:
B in G
and A20:
C in G
;
B,C are_c=-comparable
B in F
by A17, A19;
then consider n being
Element of
NAT such that A21:
B = { x where x is Point of M : dist x,(f . x) <= (dist x0,(f . x0)) * (L to_power n) }
by A5;
C in F
by A17, A20;
then consider m being
Element of
NAT such that A22:
C = { x where x is Point of M : dist x,(f . x) <= (dist x0,(f . x0)) * (L to_power m) }
by A5;
A23:
for
n,
m being
Element of
NAT st
n <= m holds
L to_power m <= L to_power n
A25:
for
n,
m being
Element of
NAT st
n <= m holds
(dist x0,(f . x0)) * (L to_power m) <= (dist x0,(f . x0)) * (L to_power n)
proof
A26:
dist x0,
(f . x0) >= 0
by METRIC_1:5;
let n,
m be
Element of
NAT ;
( n <= m implies (dist x0,(f . x0)) * (L to_power m) <= (dist x0,(f . x0)) * (L to_power n) )
assume
n <= m
;
(dist x0,(f . x0)) * (L to_power m) <= (dist x0,(f . x0)) * (L to_power n)
hence
(dist x0,(f . x0)) * (L to_power m) <= (dist x0,(f . x0)) * (L to_power n)
by A23, A26, XREAL_1:66;
verum
end;
hence
(
B c= C or
C c= B )
;
XBOOLE_0:def 9 verum
end;
then consider m being
set such that A33:
m in G
and A34:
for
C being
set st
C in G holds
m c= C
by A16, A18, FINSET_1:30;
A35:
m c= meet G
by A16, A34, SETFAM_1:6;
A36:
for
k being
Element of
NAT st
S3[
k] holds
S3[
k + 1]
proof
let k be
Element of
NAT ;
( S3[k] implies S3[k + 1] )
consider z being
Element of
{ x where x is Point of M : dist x,(f . x) <= (dist x0,(f . x0)) * (L to_power k) } ;
A37:
L * ((dist x0,(f . x0)) * (L to_power k)) =
(dist x0,(f . x0)) * (L * (L to_power k))
.=
(dist x0,(f . x0)) * ((L to_power k) * (L to_power 1))
by POWER:30
.=
(dist x0,(f . x0)) * (L to_power (k + 1))
by A1, POWER:32
;
assume
{ x where x is Point of M : dist x,(f . x) <= (dist x0,(f . x0)) * (L to_power k) } <> {}
;
S3[k + 1]
then
z in { x where x is Point of M : dist x,(f . x) <= (dist x0,(f . x0)) * (L to_power k) }
;
then consider y being
Point of
M such that
y = z
and A38:
dist y,
(f . y) <= (dist x0,(f . x0)) * (L to_power k)
;
A39:
dist (f . y),
(f . (f . y)) <= L * (dist y,(f . y))
by A3;
L * (dist y,(f . y)) <= L * ((dist x0,(f . x0)) * (L to_power k))
by A1, A38, XREAL_1:66;
then
dist (f . y),
(f . (f . y)) <= (dist x0,(f . x0)) * (L to_power (k + 1))
by A37, A39, XXREAL_0:2;
then
f . y in { x where x is Point of M : dist x,(f . x) <= (dist x0,(f . x0)) * (L to_power (k + 1)) }
;
hence
S3[
k + 1]
;
verum
end;
dist x0,
(f . x0) =
(dist x0,(f . x0)) * 1
.=
(dist x0,(f . x0)) * (L to_power 0 )
by POWER:29
;
then
x0 in { x where x is Point of M : dist x,(f . x) <= (dist x0,(f . x0)) * (L to_power 0 ) }
;
then A40:
S3[
0 ]
;
A41:
for
k being
Element of
NAT holds
S3[
k]
from NAT_1:sch 1(A40, A36);
m in F
by A17, A33;
then
m <> {}
by A5, A41;
hence
not
meet G = {}
by A35;
verum
end; then
meet F <> {}
by A4, A6, COMPTS_1:13;
then consider c9 being
Point of
(TopSpaceMetr M) such that A42:
c9 in meet F
by SUBSET_1:10;
reconsider c =
c9 as
Point of
M by A14;
reconsider r =
NAT --> (dist c,(f . c)) as
Real_Sequence ;
consider s9 being
Real_Sequence such that A43:
for
n being
Element of
NAT holds
s9 . n = H1(
n)
from SEQ_1:sch 1();
set s =
(dist x0,(f . x0)) (#) s9;
lim s9 = 0
by A1, A2, A43, SERIES_1:1;
then A44:
lim ((dist x0,(f . x0)) (#) s9) =
(dist x0,(f . x0)) * 0
by A1, A2, A43, SEQ_2:22, SERIES_1:1
.=
0
;
A45:
now let n be
Element of
NAT ;
r . n <= ((dist x0,(f . x0)) (#) s9) . ndefpred S3[
Point of
M]
means dist $1,
(f . $1) <= (dist x0,(f . x0)) * (L to_power (n + 1));
set B =
{ x where x is Point of M : S3[x] } ;
{ x where x is Point of M : S3[x] } is
Subset of
M
from DOMAIN_1:sch 7();
then
{ x where x is Point of M : S3[x] } in F
by A5, A14;
then
c in { x where x is Point of M : S3[x] }
by A42, SETFAM_1:def 1;
then A46:
ex
x being
Point of
M st
(
c = x &
dist x,
(f . x) <= (dist x0,(f . x0)) * (L to_power (n + 1)) )
;
((dist x0,(f . x0)) (#) s9) . n =
(dist x0,(f . x0)) * (s9 . n)
by SEQ_1:13
.=
(dist x0,(f . x0)) * (L to_power (n + 1))
by A43
;
hence
r . n <= ((dist x0,(f . x0)) (#) s9) . n
by A46, FUNCOP_1:13;
verum end;
(dist x0,(f . x0)) (#) s9 is
convergent
by A1, A2, A43, SEQ_2:21, SERIES_1:1;
then A47:
lim r <= lim ((dist x0,(f . x0)) (#) s9)
by A45, SEQ_2:32;
r . 0 = dist c,
(f . c)
by FUNCOP_1:13;
then
dist c,
(f . c) <= 0
by A44, A47, SEQ_4:40;
then
dist c,
(f . c) = 0
by METRIC_1:5;
hence
ex
c being
Point of
M st
dist c,
(f . c) = 0
;
verum end;
then consider c being Point of M such that
A48:
dist c,(f . c) = 0
;
take
c
; ( f . c = c & ( for x being Point of M st f . x = x holds
x = c ) )
thus A49:
f . c = c
by A48, METRIC_1:2; for x being Point of M st f . x = x holds
x = c
let x be Point of M; ( f . x = x implies x = c )
assume A50:
f . x = x
; x = c
A51:
dist x,c >= 0
by METRIC_1:5;
assume
x <> c
; contradiction
then
dist x,c <> 0
by METRIC_1:2;
then
L * (dist x,c) < dist x,c
by A2, A51, XREAL_1:159;
hence
contradiction
by A3, A49, A50; verum