let r be Real; for a, b being Real_Sequence st 0 < r & a . 0 <= b . 0 & ( for i being Nat holds
( ( a . (i + 1) = a . i & b . (i + 1) = ((a . i) + (b . i)) / 2 ) or ( a . (i + 1) = ((a . i) + (b . i)) / 2 & b . (i + 1) = b . i ) ) ) holds
ex c being Real st
( ( for j being Nat holds
( a . j <= c & c <= b . j ) ) & ex k being Nat st
( c - r < a . k & b . k < c + r ) )
let a, b be Real_Sequence; ( 0 < r & a . 0 <= b . 0 & ( for i being Nat holds
( ( a . (i + 1) = a . i & b . (i + 1) = ((a . i) + (b . i)) / 2 ) or ( a . (i + 1) = ((a . i) + (b . i)) / 2 & b . (i + 1) = b . i ) ) ) implies ex c being Real st
( ( for j being Nat holds
( a . j <= c & c <= b . j ) ) & ex k being Nat st
( c - r < a . k & b . k < c + r ) ) )
assume that
A1:
0 < r
and
A2:
a . 0 <= b . 0
and
A3:
for i being Nat holds
( ( a . (i + 1) = a . i & b . (i + 1) = ((a . i) + (b . i)) / 2 ) or ( a . (i + 1) = ((a . i) + (b . i)) / 2 & b . (i + 1) = b . i ) )
; ex c being Real st
( ( for j being Nat holds
( a . j <= c & c <= b . j ) ) & ex k being Nat st
( c - r < a . k & b . k < c + r ) )
not meet (IntervalSequence (a,b)) is empty
by A2, A3, Th32;
then consider y being object such that
A4:
y in meet (IntervalSequence (a,b))
;
A5:
y in meet (rng (IntervalSequence (a,b)))
by A4, FUNCT_6:def 4;
A6:
dom (IntervalSequence (a,b)) = NAT
by FUNCT_2:def 1;
set f = IntervalSequence (a,b);
(IntervalSequence (a,b)) . 0 in rng (IntervalSequence (a,b))
by A6, FUNCT_1:3;
then
y in (IntervalSequence (a,b)) . 0
by A5, SETFAM_1:def 1;
then A8:
y in product <*[.(a . 0),(b . 0).]*>
by Def1;
consider g being Function such that
A10:
y = g
and
dom g = dom <*[.(a . 0),(b . 0).]*>
and
for t being object st t in dom <*[.(a . 0),(b . 0).]*> holds
g . t in <*[.(a . 0),(b . 0).]*> . t
by A8, CARD_3:def 5;
y is Element of (TOP-REAL 1)
by EUCLID:22, A4;
then consider c being Real such that
A11:
y = <*c*>
by JORDAN2B:20;
take
c
; ( ( for j being Nat holds
( a . j <= c & c <= b . j ) ) & ex k being Nat st
( c - r < a . k & b . k < c + r ) )
A12:
now for i being Nat holds
( a . i <= c & c <= b . i )let i be
Nat;
( a . i <= c & c <= b . i )
(IntervalSequence (a,b)) . i in rng (IntervalSequence (a,b))
by A6, ORDINAL1:def 12, FUNCT_1:3;
then
y in (IntervalSequence (a,b)) . i
by A5, SETFAM_1:def 1;
then
y in product <*[.(a . i),(b . i).]*>
by Def1;
then consider h being
Function such that A13:
y = h
and
dom h = dom <*[.(a . i),(b . i).]*>
and A14:
for
t being
object st
t in dom <*[.(a . i),(b . i).]*> holds
h . t in <*[.(a . i),(b . i).]*> . t
by CARD_3:def 5;
A15:
dom <*[.(a . i),(b . i).]*> = Seg 1
by FINSEQ_1:def 8;
1
in Seg 1
by TARSKI:def 1, FINSEQ_1:2;
then
h . 1
in <*[.(a . i),(b . i).]*> . 1
by A14, A15;
then
g . 1
in [.(a . i),(b . i).]
by A10, A13, FINSEQ_1:def 8;
then
c in [.(a . i),(b . i).]
by A10, A11, FINSEQ_1:def 8;
hence
(
a . i <= c &
c <= b . i )
by XXREAL_1:1;
verum end;
hence
for j being Nat holds
( a . j <= c & c <= b . j )
; ex k being Nat st
( c - r < a . k & b . k < c + r )
thus
ex k being Nat st
( c - r < a . k & b . k < c + r )
verumproof
A16:
IntervalSequence (
a,
b) is
SetSequence of
(Euclid 1)
by Th17;
then A17:
for
i being
Nat holds
(
a . i <= b . i &
a . i <= a . (i + 1) &
b . (i + 1) <= b . i )
by A2, A3, Th28;
reconsider S =
IntervalSequence (
a,
b) as
non-empty pointwise_bounded closed SetSequence of
(Euclid 1) by A17, Th22;
A18:
(
diameter S is
convergent &
lim (diameter S) = 0 )
by A2, A3, Th31;
consider m0 being
Nat such that A19:
for
l being
Nat st
m0 <= l holds
|.(((diameter S) . l) - 0).| < r
by A1, A18, SEQ_2:def 7;
a . m0 <= b . m0
by A16, A2, A3, Th28;
then
(a . m0) - (a . m0) <= (b . m0) - (a . m0)
by XREAL_1:9;
then
|.((b . m0) - (a . m0)).| = (b . m0) - (a . m0)
by ABSVALUE:def 1;
then
|.(((diameter S) . m0) - 0).| = (b . m0) - (a . m0)
by A2, A3, Th28;
then A20:
(b . m0) - (a . m0) < r
by A19;
c - (a . m0) <= (b . m0) - (a . m0)
by A12, XREAL_1:9;
then A21:
c - (a . m0) < r
by A20, XXREAL_0:2;
take
m0
;
( c - r < a . m0 & b . m0 < c + r )
(c - (a . m0)) + (a . m0) < r + (a . m0)
by A21, XREAL_1:8;
then
c - r < ((a . m0) + r) - r
by XREAL_1:9;
hence
c - r < a . m0
;
b . m0 < c + r
(b . m0) - c <= (b . m0) - (a . m0)
by A12, XREAL_1:10;
then
(b . m0) - c < r
by A20, XXREAL_0:2;
then
((b . m0) - c) + c < r + c
by XREAL_1:8;
hence
b . m0 < c + r
;
verum
end;