:: Fix Point Theorem for Compact Spaces :: by Alicia de la Cruz :: :: Received July 17, 1991 :: Copyright (c) 1991-2017 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, XBOOLE_0, METRIC_1, FUNCT_1, REAL_1, CARD_1, ARYTM_3, PRE_TOPC, XXREAL_0, RELAT_1, STRUCT_0, FUNCOP_1, PCOMPS_1, RCOMP_1, SUBSET_1, POWER, SETFAM_1, TARSKI, ARYTM_1, FINSET_1, ORDINAL1, SEQ_1, VALUED_1, ORDINAL2, SEQ_2, ALI2, NAT_1, ASYMPT_1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, FINSET_1, SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, STRUCT_0, METRIC_1, PRE_TOPC, POWER, COMPTS_1, PCOMPS_1, TOPS_2, VALUED_1, SEQ_1, SEQ_2, XXREAL_0, REAL_1, NAT_1; constructors SETFAM_1, FUNCOP_1, FINSET_1, XXREAL_0, REAL_1, NAT_1, SEQ_2, POWER, TOPS_2, COMPTS_1, PCOMPS_1, VALUED_1, PARTFUN1, BINOP_2, RVSUM_1, COMSEQ_2, SEQ_1, RELSET_1; registrations SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, MEMBERED, STRUCT_0, METRIC_1, PCOMPS_1, VALUED_1, FUNCT_2, XREAL_0, SEQ_1, SEQ_2, RELSET_1, FUNCOP_1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions TARSKI, TOPS_2, ORDINAL1, XBOOLE_0, FINSET_1; equalities XBOOLE_0, SUBSET_1, STRUCT_0; theorems METRIC_1, SUBSET_1, PCOMPS_1, COMPTS_1, POWER, SEQ_2, SEQ_4, SERIES_1, SETFAM_1, SEQ_1, PRE_TOPC, TOPS_1, FINSET_1, XREAL_1, XXREAL_0, XBOOLE_0, XREAL_0, FUNCT_1, FUNCT_2; schemes SUBSET_1, SEQ_1, DOMAIN_1, NAT_1; begin definition let M be non empty MetrSpace; let f be Function of M, M; attr f is contraction means :Def1: 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; registration let M be non empty MetrSpace; cluster constant -> contraction for Function of M,M; coherence proof let f be Function of M,M such that A1: f is constant; take 1/2; thus 0<1/2 & 1/2<1; let z,y be Point of M; dom f = the carrier of M by FUNCT_2:def 1; then f.z = f.y by A1,FUNCT_1:def 10; then A2: dist(f.z,f.y) = 0 by METRIC_1:1; dist(z,y)>=0 by METRIC_1:5; hence thesis by A2; end; end; registration let M be non empty MetrSpace; cluster constant for Function of M, M; existence proof M --> the Point of M is constant; hence thesis; end; end; definition let M be non empty MetrSpace; mode Contraction of M is contraction Function of M, M; end; ::\$N Banach fixed-point theorem theorem for M being non empty MetrSpace for f being Contraction of M st 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 proof let M be non empty MetrSpace; let f be Contraction of M; set x0 = the Point of M; set a=dist(x0,f.x0); consider L being Real such that A1: 0 0; consider F being Subset-Family of TopSpaceMetr(M) such that A5: for B being Subset of TopSpaceMetr(M) holds B in F iff P[B] from SUBSET_1:sch 3; defpred P[Point of M] means dist(\$1,f.(\$1)) <= a*L to_power (0+1); A6: F is closed proof let B be Subset of TopSpaceMetr(M); 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; then consider n being Nat such that A8: B= { x where x is Point of M : dist(x,f.x) <= a*L to_power n} by A5; for x being Point of M st x in V ex r being Real st r>0 & Ball(x,r) c= V proof let x be Point of M; assume x in V; then not x in B by XBOOLE_0:def 5; then dist(x,f.x)>a*L to_power n by A8; then A9: dist(x,f.x)-a*L to_power n>0 by XREAL_1:50; take r = (dist(x,f.x)-a*L to_power n)/2; thus r>0 by A9,XREAL_1:215; let z be object; assume A10: z in Ball(x,r); then reconsider y=z as Point of M; dist(x,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 = a*L to_power n & dist(y,f.y)+2*r>dist(x,f.x) by A11,XXREAL_0:2; then not ex x being Point of M st y = x & dist(x,f.x)<= a*L to_power n by XREAL_1:19; then not y in B by A8; hence thesis by A7,SUBSET_1:29; end; then B` in Family_open_set(M) by PCOMPS_1:def 4; then B` is open by A7,PRE_TOPC:def 2; hence thesis by TOPS_1:3; 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:P[x]}is Subset of M from DOMAIN_1:sch 7; F is centered proof thus F <> {} by A5,A14,A15; defpred P[Nat] means { x where x is Point of M : dist(x,f.x) <= a*L to_power \$1}<>{}; let G be set such that A16: G <> {} and A17: G c= F and A18: G is finite; G is c=-linear proof let B,C be set; assume that A19: B in G and A20: C in G; B in F by A17,A19; then consider n being Nat such that A21: B= { x where x is Point of M : dist(x,f.x) <= a*L to_power n} by A5; C in F by A17,A20; then consider m being Nat such that A22: C= { x where x is Point of M : dist(x,f.x) <= a*L to_power m} by A5; A23: for n,m being Nat st n<=m holds L to_power m <= L to_power n proof let n,m be Nat such that A24: n<=m; per cases by A24,XXREAL_0:1; suppose n=0 by METRIC_1:5; let n,m be Nat; assume n<=m; hence thesis by A23,A26,XREAL_1:64; end; now per cases; case A27: n<=m; thus C c= B proof let y be object; assume y in C; then consider x being Point of M such that A28: y = x and A29: dist(x,f.x) <= a*L to_power m by A22; a*L to_power m <= a*L to_power n by A25,A27; then dist(x,f.x) <= a*L to_power n by A29,XXREAL_0:2; hence thesis by A21,A28; end; end; case A30: m<=n; thus B c= C proof let y be object; assume y in B; then consider x being Point of M such that A31: y = x and A32: dist(x,f.x) <= a*L to_power n by A21; a*L to_power n <= a*L to_power m by A25,A30; then dist(x,f.x) <= a*L to_power m by A32,XXREAL_0:2; hence thesis by A22,A31; end; end; end; hence B c= C or C c= B; 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 Nat st P[k] holds P[k+1] proof let k be Nat; set z = the Element of { x where x is Point of M : dist(x,f.x) <= a*L to_power k}; A37: L*(a*L to_power k)=a*(L*L to_power k) .=a*(L to_power k*L to_power 1) by POWER:25 .= a*L to_power (k+1) by A1,POWER:27; assume { x where x is Point of M : dist(x,f.x) <= a*L to_power k}<> {}; then z in { x where x is Point of M : dist(x,f.x) <= a*L to_power k}; then consider y being Point of M such that y=z and A38: dist(y,f.y)<= a*L to_power k; A39: dist(f.y,f.(f.y)) <= L*dist(y,f.y) by A3; L*dist(y,f.y) <= L*(a*L to_power k) by A1,A38,XREAL_1:64; then dist(f.y,f.(f.y)) <= a*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) <= a*L to_power (k +1)}; hence thesis; end; dist(x0,f.x0) = a*1 .= a*L to_power 0 by POWER:24; then x0 in { x where x is Point of M : dist(x,f.x) <= a*L to_power 0}; then A40: P[0]; A41: for k being Nat holds P[k] from NAT_1:sch 2(A40,A36); m in F by A17,A33; then m <> {} by A5,A41; hence thesis by A35; 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 dc = dist(c,f.c) as Element of REAL by XREAL_0:def 1; set r = seq_const dist(c,f.c); consider s9 being Real_Sequence such that A43: for n being Nat holds s9.n= F(n) from SEQ_1:sch 1; set s = a (#) s9; lim s9=0 by A1,A2,A43,SERIES_1:1; then A44: lim s = a*0 by A1,A2,A43,SEQ_2:8,SERIES_1:1 .= 0; A45: now let n be Nat; defpred P[Point of M] means dist(\$1,f.\$1) <= a*L to_power (n+1); set B = { x where x is Point of M : P[x]}; B is Subset of M from DOMAIN_1:sch 7; then B in F by A5,A14; then c in B by A42,SETFAM_1:def 1; then A46: ex x being Point of M st c = x & dist(x,f.x) <= a*L to_power ( n+1 ); s.n = a*s9.n by SEQ_1:9 .= a*L to_power (n+1) by A43; hence r.n <= s.n by A46,SEQ_1:57; end; s is convergent by A1,A2,A43,SEQ_2:7,SERIES_1:1; then A47: lim r <= lim s by A45,SEQ_2:18; r.0=dist(c,f.c) by SEQ_1:57; 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; end; then consider c being Point of M such that A48: dist(c,f.c) = 0; take c; thus A49: f.c =c by A48,METRIC_1:2; let x be Point of M; assume A50: f.x=x; A51: dist(x,c)>=0 by METRIC_1:5; assume x<>c; then dist(x,c)<>0 by METRIC_1:2; then L*dist(x,c)