:: Fix Point Theorem for Compact Spaces
:: by Alicia de la Cruz
::
:: Received July 17, 1991
:: Copyright (c) 1991-2016 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)