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