:: ALI2 semantic presentation
:: deftheorem E1 defines contraction ALI2:def 1 :
theorem :: ALI2:1
canceled;
theorem :: ALI2:2
proof
let c
1 be non
empty MetrSpace;
let c
2 be
contraction of c
1;
consider c
3 being
Real such that
E2:
( 0
< c
3 & c
3 < 1 )
and
E3:
for b
1, b
2 being
Point of c
1 holds
dist (c2 . b1),
(c2 . b2) <= c
3 * (dist b1,b2)
by E1;
assume E4:
TopSpaceMetr c
1 is
compact
;
consider c
4 being
Point of c
1;
set c
5 =
dist c
4,
(c2 . c4);
now
assume
dist c
4,
(c2 . c4) <> 0
;
defpred S
1[
set ] means ex b
1 being
Nat st a
1 = { b2 where B is Point of c1 : dist b2,(c2 . b2) <= (dist c4,(c2 . c4)) * (c3 to_power b1) } ;
consider c
6 being
Subset-Family of
(TopSpaceMetr c1) such that
E5:
for b
1 being
Subset of
(TopSpaceMetr c1) holds
( b
1 in c
6 iff S
1[b
1] )
from SUBSET_1:sch 3();
E6:
TopSpaceMetr c
1 = TopStruct the
carrier of c
1,
(Family_open_set c1)
by PCOMPS_1:def 6;
defpred S
2[
Point of c
1] means
dist a
1,
(c2 . a1) <= (dist c4,(c2 . c4)) * (c3 to_power (0 + 1));
E7:
{ b1 where B is Point of c1 : S2[b1] } is
Subset of c
1
from DOMAIN_1:sch 7();
E8:
c
6 is
centered
proof
thus
c
6 <> {}
by E5, E6, E7;
:: uses COMPTS_1:def 2
let c
7 be
set ;
assume that
E9:
c
7 <> {}
and
E10:
c
7 c= c
6
and
E11:
c
7 is
finite
;
c
7 is
c=-linear
proof
let c
8, c
9 be
set ;
:: uses ORDINAL1:def 9
assume
( c
8 in c
7 & c
9 in c
7 )
;
then E12:
( c
8 in c
6 & c
9 in c
6 )
by E10;
then consider c
10 being
Nat such that
E13:
c
8 = { b1 where B is Point of c1 : dist b1,(c2 . b1) <= (dist c4,(c2 . c4)) * (c3 to_power c10) }
by E5;
consider c
11 being
Nat such that
E14:
c
9 = { b1 where B is Point of c1 : dist b1,(c2 . b1) <= (dist c4,(c2 . c4)) * (c3 to_power c11) }
by E5, E12;
E15:
for b
1, b
2 being
Nat holds
( b
1 <= b
2 implies c
3 to_power b
2 <= c
3 to_power b
1 )
proof
let c
12, c
13 be
Nat;
assume E16:
c
12 <= c
13
;
per cases
not ( not c
12 < c
13 & not c
12 = c
13 )
by E16, REAL_1:def 5;
end;
end;
E16:
for b
1, b
2 being
Nat holds
( b
1 <= b
2 implies
(dist c4,(c2 . c4)) * (c3 to_power b2) <= (dist c4,(c2 . c4)) * (c3 to_power b1) )
now
per cases
( c
10 <= c
11 or c
11 <= c
10 )
;
case E17:
c
10 <= c
11
;
end;
case E17:
c
11 <= c
10
;
end;
end;
hence
( c
8 c= c
9 or c
9 c= c
8 )
;
:: uses XBOOLE_0:def 9
end;
then consider c
8 being
set such that
E12:
c
8 in c
7
and
E13:
for b
1 being
set holds
( b
1 in c
7 implies c
8 c= b
1 )
by E9, E11, FINSET_1:30;
E14:
c
8 c= meet c
7
by E9, E13, SETFAM_1:6;
E15:
c
8 in c
6
by E10, E12;
defpred S
3[
Nat] means
{ b1 where B is Point of c1 : dist b1,(c2 . b1) <= (dist c4,(c2 . c4)) * (c3 to_power a1) } <> {} ;
dist c
4,
(c2 . c4) =
(dist c4,(c2 . c4)) * 1
.=
(dist c4,(c2 . c4)) * (c3 to_power 0)
by POWER:29
;
then
c
4 in { b1 where B is Point of c1 : dist b1,(c2 . b1) <= (dist c4,(c2 . c4)) * (c3 to_power 0) }
;
then E16:
S
3[0]
;
E17:
for b
1 being
Nat holds
( S
3[b
1] implies S
3[b
1 + 1] )
proof
let c
9 be
Nat;
consider c
10 being
Element of
{ b1 where B is Point of c1 : dist b1,(c2 . b1) <= (dist c4,(c2 . c4)) * (c3 to_power c9) } ;
assume
{ b1 where B is Point of c1 : dist b1,(c2 . b1) <= (dist c4,(c2 . c4)) * (c3 to_power c9) } <> {}
;
then
c
10 in { b1 where B is Point of c1 : dist b1,(c2 . b1) <= (dist c4,(c2 . c4)) * (c3 to_power c9) }
;
then consider c
11 being
Point of c
1 such that
c
11 = c
10
and
E18:
dist c
11,
(c2 . c11) <= (dist c4,(c2 . c4)) * (c3 to_power c9)
;
E19:
c
3 * (dist c11,(c2 . c11)) <= c
3 * ((dist c4,(c2 . c4)) * (c3 to_power c9))
by E2, E18, XREAL_1:66;
E20: c
3 * ((dist c4,(c2 . c4)) * (c3 to_power c9)) =
(dist c4,(c2 . c4)) * (c3 * (c3 to_power c9))
.=
(dist c4,(c2 . c4)) * ((c3 to_power c9) * (c3 to_power 1))
by POWER:30
.=
(dist c4,(c2 . c4)) * (c3 to_power (c9 + 1))
by E2, POWER:32
;
dist (c2 . c11),
(c2 . (c2 . c11)) <= c
3 * (dist c11,(c2 . c11))
by E3;
then
dist (c2 . c11),
(c2 . (c2 . c11)) <= (dist c4,(c2 . c4)) * (c3 to_power (c9 + 1))
by E19, E20, XREAL_1:2;
then
c
2 . c
11 in { b1 where B is Point of c1 : dist b1,(c2 . b1) <= (dist c4,(c2 . c4)) * (c3 to_power (c9 + 1)) }
;
hence
{ b1 where B is Point of c1 : dist b1,(c2 . b1) <= (dist c4,(c2 . c4)) * (c3 to_power (c9 + 1)) } <> {}
;
end;
for b
1 being
Nat holds
S
3[b
1]
from NAT_1:sch 1(E16, E17);
then
c
8 <> {}
by E5, E15;
hence
meet c
7 <> {}
by E14, XBOOLE_1:3;
end;
c
6 is
closed
proof
let c
7 be
Subset of
(TopSpaceMetr c1);
:: uses TOPS_2:def 2
assume
c
7 in c
6
;
then consider c
8 being
Nat such that
E9:
c
7 = { b1 where B is Point of c1 : dist b1,(c2 . b1) <= (dist c4,(c2 . c4)) * (c3 to_power c8) }
by E5;
E10:
TopSpaceMetr c
1 = TopStruct the
carrier of c
1,
(Family_open_set c1)
by PCOMPS_1:def 6;
then reconsider c
9 = c
7 ` as
Subset of c
1 ;
for b
1 being
Point of c
1 holds
not ( b
1 in c
9 & for b
2 being
Real holds
not ( b
2 > 0 &
Ball b
1,b
2 c= c
9 ) )
proof
let c
10 be
Point of c
1;
assume E11:
c
10 in c
9
;
take c
11 =
((dist c10,(c2 . c10)) - ((dist c4,(c2 . c4)) * (c3 to_power c8))) / 2;
E12:
(dist c10,(c2 . c10)) - (2 * c11) = (dist c4,(c2 . c4)) * (c3 to_power c8)
;
not c
10 in c
7
by E11, SUBSET_1:54;
then
dist c
10,
(c2 . c10) > (dist c4,(c2 . c4)) * (c3 to_power c8)
by E9;
then
(dist c10,(c2 . c10)) - ((dist c4,(c2 . c4)) * (c3 to_power c8)) > 0
by XREAL_1:52;
hence
c
11 > 0
by SEQ_2:3;
let c
12 be
set ;
:: uses TARSKI:def 3
assume E13:
c
12 in Ball c
10,c
11
;
then reconsider c
13 = c
12 as
Point of c
1 ;
E14:
dist c
10,c
13 < c
11
by E13, METRIC_1:12;
(dist c10,c13) + (dist c13,(c2 . c13)) >= dist c
10,
(c2 . c13)
by METRIC_1:4;
then E15:
((dist c10,c13) + (dist c13,(c2 . c13))) + (dist (c2 . c13),(c2 . c10)) >= (dist c10,(c2 . c13)) + (dist (c2 . c13),(c2 . c10))
by XREAL_1:8;
(dist c10,(c2 . c13)) + (dist (c2 . c13),(c2 . c10)) >= dist c
10,
(c2 . c10)
by METRIC_1:4;
then E16:
((dist c13,(c2 . c13)) + (dist c10,c13)) + (dist (c2 . c13),(c2 . c10)) >= dist c
10,
(c2 . c10)
by E15, XREAL_1:2;
E17:
dist (c2 . c13),
(c2 . c10) <= c
3 * (dist c13,c10)
by E3;
dist c
13,c
10 >= 0
by METRIC_1:5;
then
c
3 * (dist c13,c10) <= dist c
13,c
10
by E2, REAL_2:147;
then
dist (c2 . c13),
(c2 . c10) <= dist c
13,c
10
by E17, XREAL_1:2;
then E18:
(dist (c2 . c13),(c2 . c10)) + (dist c13,c10) <= (dist c13,c10) + (dist c13,c10)
by XREAL_1:8;
2
* (dist c10,c13) < 2
* c
11
by E14, XREAL_1:70;
then E19:
(dist c13,(c2 . c13)) + (2 * (dist c10,c13)) < (dist c13,(c2 . c13)) + (2 * c11)
by XREAL_1:8;
(dist c13,(c2 . c13)) + ((dist c13,c10) + (dist (c2 . c13),(c2 . c10))) <= (dist c13,(c2 . c13)) + (2 * (dist c13,c10))
by E18, XREAL_1:9;
then
(dist c13,(c2 . c13)) + (2 * (dist c10,c13)) >= dist c
10,
(c2 . c10)
by E16, XREAL_1:2;
then
(dist c13,(c2 . c13)) + (2 * c11) > dist c
10,
(c2 . c10)
by E19, XREAL_1:2;
then
for b
1 being
Point of c
1 holds
not ( c
13 = b
1 &
dist b
1,
(c2 . b1) <= (dist c4,(c2 . c4)) * (c3 to_power c8) )
by E12, XREAL_1:21;
then
not c
13 in c
7
by E9;
hence
c
12 in c
9
by E10, SUBSET_1:50;
end;
then
c
7 ` in Family_open_set c
1
by PCOMPS_1:def 5;
then
c
7 ` is
open
by E10, PRE_TOPC:def 5;
hence
c
7 is
closed
by TOPS_1:29;
end;
then
meet c
6 <> {}
by E4, E8, COMPTS_1:13;
then consider c
7 being
Point of
(TopSpaceMetr c1) such that
E9:
c
7 in meet c
6
by SUBSET_1:10;
reconsider c
8 = c
7 as
Point of c
1 by E6;
deffunc H
1(
Nat)
-> Element of
REAL = c
3 to_power (a1 + 1);
consider c
9 being
Real_Sequence such that
E10:
for b
1 being
Nat holds c
9 . b
1 = H
1(b
1)
from SEQ_1:sch 1();
set c
10 =
(dist c4,(c2 . c4)) (#) c
9;
E11:
( c
9 is
convergent &
lim c
9 = 0 )
by E2, E10, SERIES_1:1;
then E12:
(dist c4,(c2 . c4)) (#) c
9 is
convergent
by SEQ_2:21;
E13:
lim ((dist c4,(c2 . c4)) (#) c9) =
(dist c4,(c2 . c4)) * 0
by E11, SEQ_2:22
.=
0
;
reconsider c
11 =
NAT --> (dist c8,(c2 . c8)) as
Real_Sequence by FUNCOP_1:57;
E14:
for b
1 being
Nat holds c
11 . b
1 = dist c
8,
(c2 . c8)
by FUNCOP_1:13;
E15:
c
11 is
convergent
by SEQ_4:39;
now
let c
12 be
Nat;
defpred S
3[
Point of c
1] means
dist a
1,
(c2 . a1) <= (dist c4,(c2 . c4)) * (c3 to_power (c12 + 1));
set c
13 =
{ b1 where B is Point of c1 : S3[b1] } ;
{ b1 where B is Point of c1 : S3[b1] } is
Subset of c
1
from DOMAIN_1:sch 7();
then
{ b1 where B is Point of c1 : S3[b1] } in c
6
by E5, E6;
then
c
8 in { b1 where B is Point of c1 : S3[b1] }
by E9, SETFAM_1:def 1;
then E16:
ex b
1 being
Point of c
1 st
( c
8 = b
1 &
dist b
1,
(c2 . b1) <= (dist c4,(c2 . c4)) * (c3 to_power (c12 + 1)) )
;
((dist c4,(c2 . c4)) (#) c9) . c
12 =
(dist c4,(c2 . c4)) * (c9 . c12)
by SEQ_1:13
.=
(dist c4,(c2 . c4)) * (c3 to_power (c12 + 1))
by E10
;
hence
c
11 . c
12 <= ((dist c4,(c2 . c4)) (#) c9) . c
12
by E14, E16;
end;
then E16:
lim c
11 <= lim ((dist c4,(c2 . c4)) (#) c9)
by E12, E15, SEQ_2:32;
c
11 . 0
= dist c
8,
(c2 . c8)
by E14;
then
(
dist c
8,
(c2 . c8) <= 0 &
dist c
8,
(c2 . c8) >= 0 )
by E13, E16, METRIC_1:5, SEQ_4:40;
then
dist c
8,
(c2 . c8) = 0
;
hence
ex b
1 being
Point of c
1 st
dist b
1,
(c2 . b1) = 0
;
end;
then consider c
6 being
Point of c
1 such that
E5:
dist c
6,
(c2 . c6) = 0
;
take
c
6
;
thus E6:
c
2 . c
6 = c
6
by E5, METRIC_1:2;
let c
7 be
Point of c
1;
assume E7:
c
2 . c
7 = c
7
;
assume
c
7 <> c
6
;
then E8:
dist c
7,c
6 <> 0
by METRIC_1:2;
dist c
7,c
6 >= 0
by METRIC_1:5;
then
c
3 * (dist c7,c6) < dist c
7,c
6
by E2, E8, REAL_2:145;
hence
not verum
by E3, E6, E7;
end;