:: ALI2 semantic presentation

begin

definition
let M be non empty MetrSpace;
let f be Function of M,M;
attrf 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 non empty V12() V17( the carrier of M) V21( the carrier of M, the carrier of M) contraction for Element of K10(K11( the carrier of M, the carrier of M));
existence
 ex b1 being Function of M,M st b1 is contraction
proof
set x = the Point of M;
reconsider f = the carrier of M --> the Point of M as Function of M,M ;
take  f ; ::_thesis: f is contraction
take  1 / 2 ; :: according to ALI2:def_1 ::_thesis: ( 0 < 1 / 2 & 1 / 2 < 1 & ( for x, y being Point of M holds dist ((f . x),(f . y)) <= (1 / 2) * (dist (x,y)) ) )
thus  ( 0 < 1 / 2 & 1 / 2 < 1 ) ; ::_thesis: for x, y being Point of M holds dist ((f . x),(f . y)) <= (1 / 2) * (dist (x,y))
let z, y be Point of M; ::_thesis: dist ((f . z),(f . y)) <= (1 / 2) * (dist (z,y))
 ( f . z = the Point of M & f . y = the Point of M ) by FUNCOP_1:7;
then A1: dist ((f . z),(f . y)) = 0 by METRIC_1:1;
 dist (z,y) >= 0 by METRIC_1:5;
hence  dist ((f . z),(f . y)) <= (1 / 2) * (dist (z,y)) by A1; ::_thesis: verum
end;
end;

definition
let M be non empty MetrSpace;
mode Contraction of M is contraction Function of M,M;
end;

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
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 ) ) )
set x0 = the Point of M;
set a = dist ( the Point of M,(f . the Point of M));
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 ; ::_thesis: ex c being Point of M st
( f . c = c & ( for x being Point of M st f . x = x holds
x = c ) )
now__::_thesis:_(_dist_(_the_Point_of_M,(f_._the_Point_of_M))_<>_0_implies_ex_c_being_Point_of_M_st_dist_(c,(f_._c))_=_0_)
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 ( the Point of M,(f . the Point of M))) * (L to_power n)  }  ;
assume  dist ( the Point of M,(f . the Point of M)) <> 0 ; ::_thesis: 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 ( the Point of M,(f . the Point of M))) * (L to_power (0 + 1));
A6: 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 )
A7: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5;
then reconsider V = B ` as Subset of M ;
assume  B in F ; ::_thesis: 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 ( the Point of M,(f . the Point of M))) * (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; ::_thesis: ( x in V implies ex r being Real st
( r > 0 & Ball (x,r) c= V ) )
assume  x in V ; ::_thesis: 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 ( the Point of M,(f . the Point of M))) * (L to_power n) by A8;
then A9: (dist (x,(f . x))) - ((dist ( the Point of M,(f . the Point of M))) * (L to_power n)) > 0 by XREAL_1:50;
take r = ((dist (x,(f . x))) - ((dist ( the Point of M,(f . the Point of M))) * (L to_power n))) / 2; ::_thesis: ( r > 0 & Ball (x,r) c= V )
thus  r > 0 by A9, XREAL_1:215; ::_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 A10: z in Ball (x,r) ; ::_thesis: z in V
then reconsider y = z as Point of M ;
 dist (x,y) < r by A10, METRIC_1:11;
then  2 * (dist (x,y)) < 2 * r by XREAL_1:68;
then A11: (dist (y,(f . y))) + (2 * (dist (x,y))) < (dist (y,(f . y))) + (2 * r) by XREAL_1:6;
 (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:6;
 ( dist ((f . y),(f . x)) <= L * (dist (y,x)) & L * (dist (y,x)) <= dist (y,x) ) by A2, A3, METRIC_1:5, XREAL_1:153;
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:6;
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:7;
 (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 ( the Point of M,(f . the Point of M))) * (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 ( the Point of M,(f . the Point of M))) * (L to_power n) ) by XREAL_1:19;
then  not y in B by A8;
hence  z in V by A7, SUBSET_1:29; ::_thesis: verum
end;
then  B ` in Family_open_set M by PCOMPS_1:def_4;
then  B ` is open by A7, PRE_TOPC:def_2;
hence  B is closed by TOPS_1:3; ::_thesis: verum
end;
A14: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def_5;
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; :: 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 = {} )
defpred S3[ Element of NAT ] means  {  x where x is Point of M : dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power $1)  }  <> {} ;
let G be set ; ::_thesis: ( 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 ; ::_thesis: not meet G = {}
 G is c=-linear
proof
let B, C be set ; :: according to ORDINAL1:def_8 ::_thesis: ( 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 ; ::_thesis: 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 ( the Point of M,(f . the Point of M))) * (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 ( the Point of M,(f . the Point of M))) * (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
proof
let n, m be Element of NAT ; ::_thesis: ( n <= m implies L to_power m <= L to_power n )
assume A24: n <= m ; ::_thesis: L to_power m <= L to_power n
percases ( n < m or n = m ) by A24, XXREAL_0:1;
suppose n < m ; ::_thesis: L to_power m <= L to_power n
hence  L to_power m <= L to_power n by A1, A2, POWER:40; ::_thesis: verum
end;
suppose n = m ; ::_thesis: L to_power m <= L to_power n
hence  L to_power m <= L to_power n ; ::_thesis: verum
end;
end;
end;
A25: for n, m being Element of NAT st n <= m holds
(dist ( the Point of M,(f . the Point of M))) * (L to_power m) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power n)
proof
A26: dist ( the Point of M,(f . the Point of M)) >= 0 by METRIC_1:5;
let n, m be Element of NAT ; ::_thesis: ( n <= m implies (dist ( the Point of M,(f . the Point of M))) * (L to_power m) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power n) )
assume  n <= m ; ::_thesis: (dist ( the Point of M,(f . the Point of M))) * (L to_power m) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power n)
hence  (dist ( the Point of M,(f . the Point of M))) * (L to_power m) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power n) by A23, A26, XREAL_1:64; ::_thesis: verum
end;
now__::_thesis:_(_(_n_<=_m_&_C_c=_B_)_or_(_m_<=_n_&_B_c=_C_)_)
percases ( n <= m or m <= n ) ;
caseA27: n <= m ; ::_thesis: C c= B
thus  C c= B ::_thesis: verum
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in C or y in B )
assume  y in C ; ::_thesis: y in B
then consider x being Point of M such that
A28: y = x and
A29: dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power m) by A22;
 (dist ( the Point of M,(f . the Point of M))) * (L to_power m) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power n) by A25, A27;
then  dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power n) by A29, XXREAL_0:2;
hence  y in B by A21, A28; ::_thesis: verum
end;
end;
caseA30: m <= n ; ::_thesis: B c= C
thus  B c= C ::_thesis: verum
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in B or y in C )
assume  y in B ; ::_thesis: y in C
then consider x being Point of M such that
A31: y = x and
A32: dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power n) by A21;
 (dist ( the Point of M,(f . the Point of M))) * (L to_power n) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power m) by A25, A30;
then  dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power m) by A32, XXREAL_0:2;
hence  y in C by A22, A31; ::_thesis: verum
end;
end;
end;
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
A33: m in G and
A34: for C being set st C in G holds
m c= C by A16, A18, FINSET_1:11;
A35: m c= meet G by A16, A34, SETFAM_1:5;
A36: 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] )
set z = the Element of  {  x where x is Point of M : dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power k)  }  ;
A37: L * ((dist ( the Point of M,(f . the Point of M))) * (L to_power k)) = (dist ( the Point of M,(f . the Point of M))) * (L * (L to_power k))
.= (dist ( the Point of M,(f . the Point of M))) * ((L to_power k) * (L to_power 1)) by POWER:25
.= (dist ( the Point of M,(f . the Point of M))) * (L to_power (k + 1)) by A1, POWER:27 ;
assume   {  x where x is Point of M : dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power k)  }  <> {} ; ::_thesis: S3[k + 1]
then  the Element of  {  x where x is Point of M : dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power k)  }  in  {  x where x is Point of M : dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power k)  }  ;
then consider y being Point of M such that
 y = the Element of  {  x where x is Point of M : dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (L to_power k)  }  and
A38: dist (y,(f . y)) <= (dist ( the Point of M,(f . the Point of M))) * (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 ( the Point of M,(f . the Point of M))) * (L to_power k)) by A1, A38, XREAL_1:64;
then  dist ((f . y),(f . (f . y))) <= (dist ( the Point of M,(f . the Point of M))) * (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 ( the Point of M,(f . the Point of M))) * (L to_power (k + 1))  }  ;
hence  S3[k + 1] ; ::_thesis: verum
end;
dist ( the Point of M,(f . the Point of M)) = (dist ( the Point of M,(f . the Point of M))) * 1
.= (dist ( the Point of M,(f . the Point of M))) * (L to_power 0) by POWER:24 ;
then  the Point of M in  {  x where x is Point of M : dist (x,(f . x)) <= (dist ( the Point of M,(f . the Point of M))) * (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; ::_thesis: verum
end;
then  meet F <> {} by A4, A6, COMPTS_1:4;
then consider c9 being Point of (TopSpaceMetr M) such that
A42: c9 in meet F by SUBSET_1:4;
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 ( the Point of M,(f . the Point of M))) (#) s9;
 lim s9 = 0 by A1, A2, A43, SERIES_1:1;
then A44: lim ((dist ( the Point of M,(f . the Point of M))) (#) s9) = (dist ( the Point of M,(f . the Point of M))) * 0 by A1, A2, A43, SEQ_2:8, SERIES_1:1
.= 0 ;
A45: now__::_thesis:_for_n_being_Element_of_NAT_holds_r_._n_<=_((dist_(_the_Point_of_M,(f_._the_Point_of_M)))_(#)_s9)_._n
let n be Element of NAT ; ::_thesis: r . n <= ((dist ( the Point of M,(f . the Point of M))) (#) s9) . n
defpred S3[ Point of M] means  dist ($1,(f . $1)) <= (dist ( the Point of M,(f . the Point of M))) * (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 ( the Point of M,(f . the Point of M))) * (L to_power (n + 1)) ) ;
((dist ( the Point of M,(f . the Point of M))) (#) s9) . n = (dist ( the Point of M,(f . the Point of M))) * (s9 . n) by SEQ_1:9
.= (dist ( the Point of M,(f . the Point of M))) * (L to_power (n + 1)) by A43 ;
hence  r . n <= ((dist ( the Point of M,(f . the Point of M))) (#) s9) . n by A46, FUNCOP_1:7; ::_thesis: verum
end;
 (dist ( the Point of M,(f . the Point of M))) (#) s9 is convergent by A1, A2, A43, SEQ_2:7, SERIES_1:1;
then A47: lim r <= lim ((dist ( the Point of M,(f . the Point of M))) (#) s9) by A45, SEQ_2:18;
 r . 0 = dist (c,(f . c)) by FUNCOP_1:7;
then  dist (c,(f . c)) <= 0 by A44, A47, SEQ_4:25;
then  dist (c,(f . c)) = 0 by METRIC_1:5;
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
A48: 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 A49: f . c = c by A48, 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 A50: f . x = x ; ::_thesis: x = c
A51: dist (x,c) >= 0 by METRIC_1:5;
assume  x <> c ; ::_thesis: contradiction
then  dist (x,c) <> 0 by METRIC_1:2;
then  L * (dist (x,c)) < dist (x,c) by A2, A51, XREAL_1:157;
hence  contradiction by A3, A49, A50; ::_thesis: verum
end;