:: 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;