Copyright (c) 1991 Association of Mizar Users
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;