### The Mizar article:

### Fix Point Theorem for Compact Spaces

**by****Alicia de la Cruz**

- Received July 17, 1991
Copyright (c) 1991 Association of Mizar Users

- MML identifier: ALI2
- [ MML identifier index ]

environ vocabulary METRIC_1, FINSET_1, BOOLE, ZFMISC_1, FUNCT_1, PRE_TOPC, FUNCOP_1, RELAT_1, ARYTM_3, PCOMPS_1, COMPTS_1, SETFAM_1, POWER, SUBSET_1, ARYTM_1, SEQ_1, SEQ_2, ORDINAL2, SEQM_3, ALI2, HAHNBAN; notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XREAL_0, FINSET_1, SETFAM_1, METRIC_1, RELAT_1, FUNCT_2, STRUCT_0, PRE_TOPC, POWER, FUNCOP_1, COMPTS_1, PCOMPS_1, TOPS_2, SEQ_1, SEQ_2, SEQM_3, REAL_1, NAT_1; constructors FINSET_1, POWER, FUNCOP_1, COMPTS_1, PCOMPS_1, TOPS_2, SEQ_2, SEQM_3, REAL_1, NAT_1, PARTFUN1, MEMBERED; clusters STRUCT_0, PCOMPS_1, FUNCOP_1, XREAL_0, SEQ_1, METRIC_1, MEMBERED, ZFMISC_1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions COMPTS_1, TARSKI, TOPS_2, ORDINAL1, XBOOLE_0; theorems METRIC_1, SUBSET_1, REAL_1, PCOMPS_1, REAL_2, COMPTS_1, POWER, SEQ_2, SEQ_4, SERIES_1, SEQM_3, AXIOMS, SETFAM_1, TARSKI, SEQ_1, PRE_TOPC, TOPS_1, SQUARE_1, FUNCOP_1, FUNCT_2, RELSET_1, ORDINAL1, XBOOLE_0, XBOOLE_1, XCMPLX_1; schemes SETFAM_1, SEQ_1, DOMAIN_1, FINSET_1, NAT_1; begin reserve M for non empty MetrSpace; theorem Th1: for F being set st F is finite & F <> {} & F is c=-linear ex m being set st m in F & for C being set st C in F holds m c= C proof defpred P[set] means $1 <> {} implies ex m being set st m in $1 & for C being set st C in $1 holds m c= C; let F be set such that A1: F is finite and A2: F <> {} and A3: F is c=-linear; A4: P[{}]; A5: now let x,B be set such that A6:x in F & B c= F & P[B]; now per cases; :: we have to prove P[BU{x}] suppose A7:not ex y being set st y in B & y c=x; assume B \/ {x} <> {}; take m = x; x in {x} by TARSKI:def 1; hence m in B \/ {x} by XBOOLE_0:def 2; let C be set; assume C in B \/ {x}; then A8: C in B or C in {x} by XBOOLE_0:def 2; then C,x are_c=-comparable by A3,A6,ORDINAL1:def 9,TARSKI:def 1; then C c= x or x c= C by XBOOLE_0:def 9; hence m c= C by A7,A8,TARSKI:def 1; suppose ex y being set st y in B & y c=x; then consider y being set such that A9: y in B & y c=x; assume B \/ {x} <> {}; consider m being set such that A10:m in B and A11: for C being set st C in B holds m c= C by A6,A9; m c= y by A9,A11; then A12:m c= x by A9,XBOOLE_1:1; take m; thus m in B \/ {x} by A10,XBOOLE_0:def 2; let C be set; assume C in B \/ {x}; then C in B or C in {x} by XBOOLE_0:def 2; hence m c= C by A11,A12,TARSKI:def 1; end; hence P[B \/ {x}]; end; P[F] from Finite(A1,A4,A5); hence thesis by A2; end; definition let M be non empty MetrSpace; mode contraction of M -> Function of the carrier of M, the carrier of M means :Def1: ex L being Real st 0 < L & L < 1 & for x,y being Point of M holds dist(it.x,it.y) <= L*dist(x,y); existence proof consider x being Point of M; (the carrier of M) --> x is Function of the carrier of M, the carrier of M proof A1: dom ((the carrier of M) --> x) = the carrier of M by FUNCOP_1:19; rng ((the carrier of M) --> x) c= {x} by FUNCOP_1:19; then rng ((the carrier of M) --> x) c= the carrier of M by XBOOLE_1:1; hence thesis by A1,FUNCT_2:def 1,RELSET_1:11; end; then reconsider f = (the carrier of M) --> x as Function of the carrier of M, the carrier of M; take f, 1/2; thus 0<1/2 & 1/2<1; let z,y be Point of M; f.z=x & f.y=x by FUNCOP_1:13; then A2: 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 A2,REAL_2:121; end; end; theorem for f being contraction of M st TopSpaceMetr(M) is compact ex c being Point of M st f.c =c & :: exists a fix point for x being Point of M st f.x=x holds x=c :: exactly 1 fix point proof let f be contraction of M; 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; consider x0 being Point of M; set a=dist(x0,f.x0); now assume a <> 0; defpred _P[set] means ex n being Nat st $1 = { x where x is Point of M : dist(x,f.x) <= a*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 _P[B] from SubFamEx; A5: TopSpaceMetr(M)=TopStruct (#the carrier of M,Family_open_set(M)#) by PCOMPS_1:def 6; defpred _P[Point of M] means dist($1,f.($1)) <= a*L to_power (0+1); A6: {x where x is Point of M:_P[x]}is Subset of M from SubsetD; A7: F is centered proof thus F <> {} by A4,A5,A6; let G be set such that A8: G <> {} and A9: G c= F and A10: G is finite; G is c=-linear proof let B,C be set; assume B in G & C in G; then A11:B in F & C in F by A9; then consider n being Nat such that A12: B= { x where x is Point of M : dist(x,f.x) <= a*L to_power n} by A4; consider m being Nat such that A13: C= { x where x is Point of M : dist(x,f.x) <= a*L to_power m} by A4,A11; A14: 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 A15:n<=m; now per cases by A15,REAL_1:def 5; suppose n<m; hence L to_power n >= L to_power m by A1,POWER:45; suppose n=m; hence L to_power n >= L to_power m; end; hence thesis; end; A16: for n,m being Nat st n<=m holds a*L to_power m <= a*L to_power n proof let n,m be Nat such that A17:n<=m; A18:a>=0 by METRIC_1:5; L to_power m <= L to_power n by A14,A17; hence a*L to_power m <= a*L to_power n by A18,AXIOMS:25; end; now per cases; case A19:n<=m; thus C c= B proof let y be set; assume y in C; then consider x being Point of M such that A20: y = x and A21: dist(x,f.x) <= a*L to_power m by A13; a*L to_power m <= a*L to_power n by A16,A19; then dist(x,f.x) <= a*L to_power n by A21,AXIOMS:22; hence y in B by A12,A20; end; case A22:m<=n; thus B c= C proof let y be set; assume y in B; then consider x being Point of M such that A23: y = x and A24: dist(x,f.x) <= a*L to_power n by A12; a*L to_power n <= a*L to_power m by A16,A22; then dist(x,f.x) <= a*L to_power m by A24,AXIOMS:22; hence y in C by A13,A23; end; end; hence B c= C or C c= B; end; then consider m being set such that A25: m in G and A26: for C being set st C in G holds m c= C by A8,A10,Th1; A27: m c= meet G by A8,A26,SETFAM_1:6; A28: m in F by A9,A25; defpred _P[Nat] means { x where x is Point of M : dist(x,f.x) <= a*L to_power $1}<>{}; dist(x0,f.x0) = a*1 .= a*L to_power 0 by POWER:29; then x0 in { x where x is Point of M : dist(x,f.x) <= a*L to_power 0}; then A29: _P[0]; A30:for k being Nat st _P[k] holds _P[k+1] proof let k be Nat; consider z being Element of { x where x is Point of M : dist(x,f.x) <= a*L to_power k}; 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 A31:dist(y,f.y)<= a*L to_power k; A32:L*dist(y,f.y) <= L*(a*L to_power k) by A1,A31,AXIOMS:25; A33:L*(a*L to_power k)=a*(L*L to_power k) by XCMPLX_1:4 .=a*(L to_power k*L to_power 1) by POWER:30 .= a*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)) <= a*L to_power (k+1) by A32,A33,AXIOMS:22; then f.y in { x where x is Point of M : dist(x,f.x) <= a*L to_power (k+1)}; hence { x where x is Point of M : dist(x,f.x) <= a*L to_power (k+1)}<>{}; end; for k being Nat holds _P[k] from Ind(A29,A30); then m <> {} by A4,A28; hence meet G <> {} by A27,XBOOLE_1:3; end; F is closed proof let B be Subset of TopSpaceMetr(M); assume B in F; then consider n being Nat such that A34:B= { x where x is Point of M : dist(x,f.x) <= a*L to_power n} by A4; A35: 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 ex r being Real st r>0 & Ball(x,r) c= V proof let x be Point of M such that A36:x in V; take r = (dist(x,f.x)-a*L to_power n)/2; 2*r = dist(x,f.x)-a*L to_power n by XCMPLX_1:88; then A37: dist(x,f.x)-2*r = a*L to_power n by XCMPLX_1:18; not x in B by A36,SUBSET_1:54; then dist(x,f.x)>a*L to_power n by A34; then dist(x,f.x)-a*L to_power n>0 by SQUARE_1:11; hence r>0 by SEQ_2:3; let z be set; assume A38:z in Ball(x,r); then reconsider y=z as Point of M; A39: dist(x,y)<r by A38,METRIC_1:12; dist(x,y) + dist(y,f.y) >= dist(x,f.y) by METRIC_1:4; then A40: (dist(x,y) + dist(y,f.y)) + dist(f.y,f.x) >= dist(x,f.y) + dist(f.y,f.x) by AXIOMS:24; 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 A40,AXIOMS:22; then A41: dist(y,f.y)+(dist(x,y)+dist(f.y,f.x))>=dist(x,f.x) by XCMPLX_1:1; A42: dist(f.y,f.x)<=L*dist(y,x) by A2; dist(y,x)>=0 by METRIC_1:5; then L*dist(y,x)<=dist(y,x) by A1,REAL_2:147; then dist(f.y,f.x)<=dist(y,x) by A42,AXIOMS:22; then A43: dist(f.y,f.x)+dist(y,x) <= dist(y,x)+dist(y,x) by AXIOMS:24; 2*dist(x,y)<2*r by A39,REAL_1:70; then A44: dist(y,f.y) + 2*dist(x,y)< dist(y,f.y) + 2*r by REAL_1:53; dist(y,x) + dist(f.y,f.x) <= 2*dist(y,x) by A43,XCMPLX_1:11; then dist(y,f.y) + (dist(y,x) + dist(f.y,f.x)) <= dist(y,f.y) + 2*dist(y,x) by REAL_1:55; then dist(y,f.y)+2*dist(x,y)>=dist(x,f.x) by A41,AXIOMS:22; then dist(y,f.y)+2*r>dist(x,f.x) by A44,AXIOMS:22; then not ex x being Point of M st y = x & dist(x,f.x)<= a*L to_power n by A37,REAL_1:84; then not y in B by A34; hence z in V by A35,SUBSET_1:50; end; then B` in Family_open_set(M) by PCOMPS_1:def 5; then B` in Family_open_set(M); then B` is open by A35,PRE_TOPC:def 5; hence B is closed by TOPS_1:29; end; then meet F <> {} by A3,A7,COMPTS_1:13; then consider c' being Point of TopSpaceMetr(M) such that A45: c' in meet F by SUBSET_1:10; reconsider c = c' as Point of M by A5; deffunc _F(Nat) = L to_power ($1+1); consider s' being Real_Sequence such that A46:for n being Nat holds s'.n= _F(n) from ExRealSeq; set s = a (#) s'; A47: s' is convergent & lim s'=0 by A1,A46,SERIES_1:1; then A48: s is convergent by SEQ_2:21; A49: lim s = a*0 by A47,SEQ_2:22 .= 0; deffunc _F(set) = dist(c,f.c); consider r being Real_Sequence such that A50: for n being Nat holds r.n=_F(n) from ExRealSeq; A51: r is constant by A50,SEQM_3:def 6; then A52: r is convergent by SEQ_4:39; 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 SubsetD; then B in F by A4,A5; then c in B by A45,SETFAM_1:def 1; then A53: ex x being Point of M st c = x & dist(x,f.x) <= a*L to_power (n+1 ); s.n = a*s'.n by SEQ_1:13 .= a*L to_power (n+1) by A46; hence r.n <= s.n by A50,A53; end; then A54: lim r <= lim s by A48,A52,SEQ_2:32; r.0=dist(c,f.c) by A50; then dist(c,f.c)<=0 & dist(c,f.c)>=0 by A49,A51,A54,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; end; then consider c being Point of M such that A55: dist(c,f.c) = 0; take c; thus A56: f.c =c by A55,METRIC_1:2; let x be Point of M; assume A57: f.x=x; assume x<>c; then A58: 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,A58,REAL_2:145; hence contradiction by A2,A56,A57; end;

Back to top