let a, b be Real_Sequence; ( ( for i being Nat holds
( a . i <= b . i & a . i <= a . (i + 1) & b . (i + 1) <= b . i ) ) implies IntervalSequence (a,b) is non-empty pointwise_bounded closed SetSequence of (Euclid 1) )
assume A1:
for i being Nat holds
( a . i <= b . i & a . i <= a . (i + 1) & b . (i + 1) <= b . i )
; IntervalSequence (a,b) is non-empty pointwise_bounded closed SetSequence of (Euclid 1)
reconsider s = IntervalSequence (a,b) as SetSequence of (Euclid 1) by Th17;
A2:
s is non-empty
proof
assume
not
s is
non-empty
;
contradiction
then consider i being
object such that A3:
i in dom s
and A4:
s . i = {}
;
product <*[.(a . i),(b . i).]*> = {}
by A3, A4, Def1;
then
{} in rng <*[.(a . i),(b . i).]*>
by CARD_3:26;
then consider j being
object such that A5:
j in dom <*[.(a . i),(b . i).]*>
and A6:
<*[.(a . i),(b . i).]*> . j = {}
by FUNCT_1:def 3;
j in {1}
by FINSEQ_1:2, A5, FINSEQ_1:def 8;
then
<*[.(a . i),(b . i).]*> . 1
= {}
by A6, TARSKI:def 1;
then
[.(a . i),(b . i).] is
empty
by FINSEQ_1:def 8;
hence
contradiction
by A1, A3, XXREAL_1:30;
verum
end;
A7:
s is pointwise_bounded
proof
now for i being Nat holds s . i is bounded let i be
Nat;
s . i is bounded A8:
s . i = product <*[.(a . i),(b . i).]*>
by Def1;
set si =
product <*[.(a . i),(b . i).]*>;
reconsider si =
product <*[.(a . i),(b . i).]*> as
Subset of
(Euclid 1) by A8;
ex
r being
Real st
(
0 < r & ( for
x,
y being
Point of
(Euclid 1) st
x in si &
y in si holds
dist (
x,
y)
<= r ) )
proof
set r =
(b . i) - (a . i);
per cases
( (b . i) - (a . i) = 0 or 0 < (b . i) - (a . i) )
by A1, XREAL_1:48;
suppose A11:
0 < (b . i) - (a . i)
;
ex r being Real st
( 0 < r & ( for x, y being Point of (Euclid 1) st x in si & y in si holds
dist (x,y) <= r ) )take
(b . i) - (a . i)
;
( 0 < (b . i) - (a . i) & ( for x, y being Point of (Euclid 1) st x in si & y in si holds
dist (x,y) <= (b . i) - (a . i) ) )thus
0 < (b . i) - (a . i)
by A11;
for x, y being Point of (Euclid 1) st x in si & y in si holds
dist (x,y) <= (b . i) - (a . i)hereby verum
let x,
y be
Point of
(Euclid 1);
( x in si & y in si implies dist (x,y) <= (b . i) - (a . i) )assume that A12:
x in si
and A13:
y in si
;
dist (x,y) <= (b . i) - (a . i)consider gx being
Function such that A14:
x = gx
and
dom gx = dom <*[.(a . i),(b . i).]*>
and A15:
for
j being
object st
j in dom <*[.(a . i),(b . i).]*> holds
gx . j in <*[.(a . i),(b . i).]*> . j
by A12, CARD_3:def 5;
consider gy being
Function such that A16:
y = gy
and
dom gy = dom <*[.(a . i),(b . i).]*>
and A17:
for
j being
object st
j in dom <*[.(a . i),(b . i).]*> holds
gy . j in <*[.(a . i),(b . i).]*> . j
by A13, CARD_3:def 5;
(
x in Euclid 1 &
y in Euclid 1 )
;
then
(
x in TOP-REAL 1 &
y in TOP-REAL 1 )
by EUCLID:67;
then reconsider rx =
x,
ry =
y as
Element of
REAL 1
by EUCLID:22;
Euclid 1
= MetrStruct(#
(REAL 1),
(Pitag_dist 1) #)
by EUCLID:def 7;
then A18:
dist (
x,
y)
= |.(rx - ry).|
by EUCLID:def 6;
consider ux being
Real such that A19:
rx = <*ux*>
by Th6;
consider uy being
Real such that A20:
ry = <*uy*>
by Th6;
(
rx = 1
|-> ux &
ry = 1
|-> uy )
by A19, A20, FINSEQ_2:59;
then A21:
|.(rx - ry).| =
(sqrt 1) * |.(ux - uy).|
by TOPREALC:11
.=
|.(ux - uy).|
by SQUARE_1:18
;
1
in Seg 1
by TARSKI:def 1, FINSEQ_1:2;
then
1
in dom <*[.(a . i),(b . i).]*>
by FINSEQ_1:def 8;
then
(
gx . 1
in <*[.(a . i),(b . i).]*> . 1 &
gy . 1
in <*[.(a . i),(b . i).]*> . 1 )
by A15, A17;
then
(
gx . 1
in [.(a . i),(b . i).] &
gy . 1
in [.(a . i),(b . i).] )
by FINSEQ_1:def 8;
then
(
ux in [.(a . i),(b . i).] &
uy in [.(a . i),(b . i).] )
by A14, A16, A19, A20, FINSEQ_1:def 8;
hence
dist (
x,
y)
<= (b . i) - (a . i)
by A21, A18, UNIFORM1:12;
verum
end; end; end;
end; then
si is
bounded
;
hence
s . i is
bounded
by Def1;
verum end;
hence
s is
pointwise_bounded
by COMPL_SP:def 1;
verum
end;
s is closed
proof
for
i being
Nat holds
s . i is
closed
proof
let i be
Nat;
s . i is closed
A22:
s . i = product <*[.(a . i),(b . i).]*>
by Def1;
then reconsider si =
product <*[.(a . i),(b . i).]*> as
Subset of
(Euclid 1) ;
A23:
si ` = product <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*>
si ` is
open
proof
si ` in Family_open_set (Euclid 1)
proof
for
x being
Element of
(Euclid 1) st
x in si ` holds
ex
r being
Real st
(
r > 0 &
Ball (
x,
r)
c= si ` )
proof
let x be
Element of
(Euclid 1);
( x in si ` implies ex r being Real st
( r > 0 & Ball (x,r) c= si ` ) )
assume A24:
x in si `
;
ex r being Real st
( r > 0 & Ball (x,r) c= si ` )
set A =
].-infty,(a . i).[;
set B =
].(b . i),+infty.[;
set f =
<*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*>;
consider g being
Function such that A25:
x = g
and
dom g = dom <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*>
and A26:
for
j being
object st
j in dom <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> holds
g . j in <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> . j
by A24, A23, CARD_3:def 5;
1
in Seg 1
by TARSKI:def 1, FINSEQ_1:2;
then
1
in dom <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*>
by FINSEQ_1:def 8;
then
g . 1
in <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> . 1
by A26;
then
g . 1
in ].-infty,(a . i).[ \/ ].(b . i),+infty.[
by FINSEQ_1:def 8;
per cases then
( g . 1 in ].-infty,(a . i).[ or g . 1 in ].(b . i),+infty.[ )
by XBOOLE_0:def 3;
suppose A27:
g . 1
in ].-infty,(a . i).[
;
ex r being Real st
( r > 0 & Ball (x,r) c= si ` )then reconsider g1 =
g . 1 as
ExtReal ;
now ex r being object st
( r > 0 & Ball (x,r) c= si ` )
x is
Element of
(TOP-REAL 1)
by EUCLID:67;
then
x is
Element of
REAL 1
by EUCLID:22;
then
x in REAL 1
;
then
x in 1
-tuples_on REAL
by EUCLID:def 1;
then
g in Funcs (
(Seg 1),
REAL)
by A25, FINSEQ_2:93;
then consider h being
Function such that A28:
g = h
and A29:
dom h = Seg 1
and A30:
rng h c= REAL
by FUNCT_2:def 2;
1
in dom h
by A29, TARSKI:def 1, FINSEQ_1:2;
then
h . 1
in REAL
by A30, FUNCT_1:3;
then reconsider g1 =
g1 as
Real by A28;
set r =
|.(g1 - (a . i)).|;
take r =
|.(g1 - (a . i)).|;
( r > 0 & Ball (x,r) c= si ` )
g1 - (a . i) <> 0
by A27, XXREAL_1:233;
hence
r > 0
;
Ball (x,r) c= si ` thus
Ball (
x,
r)
c= si `
verumproof
let t be
object ;
TARSKI:def 3 ( not t in Ball (x,r) or t in si ` )
assume A31:
t in Ball (
x,
r)
;
t in si `
then reconsider t1 =
t as
Element of
(Euclid 1) ;
(
t1 in Euclid 1 &
x in Euclid 1 )
;
then
(
t1 in TOP-REAL 1 &
x in TOP-REAL 1 )
by EUCLID:67;
then reconsider rt1 =
t1,
rx =
x as
Element of
REAL 1
by EUCLID:22;
Euclid 1
= MetrStruct(#
(REAL 1),
(Pitag_dist 1) #)
by EUCLID:def 7;
then A32:
dist (
x,
t1)
= |.(rx - rt1).|
by EUCLID:def 6;
now ex rt1 being Element of REAL 1 st
( t = rt1 & dom rt1 = dom <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> & ( for j being object st j in dom <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> holds
rt1 . j in <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> . j ) )take rt1 =
rt1;
( t = rt1 & dom rt1 = dom <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> & ( for j being object st j in dom <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> holds
rt1 . j in <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> . j ) )thus
t = rt1
;
( dom rt1 = dom <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> & ( for j being object st j in dom <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> holds
rt1 . j in <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> . j ) )
rt1 in REAL 1
;
then
rt1 in 1
-tuples_on REAL
by EUCLID:def 1;
then
rt1 in Funcs (
(Seg 1),
REAL)
by FINSEQ_2:93;
then consider h being
Function such that A33:
rt1 = h
and A34:
dom h = Seg 1
and
rng h c= REAL
by FUNCT_2:def 2;
thus
dom rt1 = dom <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*>
by A33, A34, FINSEQ_1:def 8;
for j being object st j in dom <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> holds
rt1 . j in <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> . jhereby verum
let j be
object ;
( j in dom <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> implies rt1 . j in <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> . j )assume
j in dom <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*>
;
rt1 . j in <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> . jthen A35:
j in {1}
by FINSEQ_1:2, FINSEQ_1:def 8;
then A36:
j = 1
by TARSKI:def 1;
consider rt2 being
Real such that A37:
rt1 = <*rt2*>
by Th6;
A38:
rt1 . j =
rt1 . 1
by A35, TARSKI:def 1
.=
rt2
by A37, FINSEQ_1:def 8
;
consider ux being
Real such that A39:
rx = <*ux*>
by Th6;
(
rx = 1
|-> ux &
rt1 = 1
|-> rt2 )
by A37, A39, FINSEQ_2:59;
then A40:
|.(rx - rt1).| =
(sqrt 1) * |.(ux - rt2).|
by TOPREALC:11
.=
|.(ux - rt2).|
by SQUARE_1:18
;
rt2 in ].-infty,(a . i).[ \/ ].(b . i),+infty.[
hence
rt1 . j in <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> . j
by A36, FINSEQ_1:def 8, A38;
verum
end; end;
hence
t in si `
by A23, CARD_3:def 5;
verum
end; end; hence
ex
r being
Real st
(
r > 0 &
Ball (
x,
r)
c= si ` )
;
verum end; suppose A43:
g . 1
in ].(b . i),+infty.[
;
ex r being Real st
( r > 0 & Ball (x,r) c= si ` )then reconsider g1 =
g . 1 as
ExtReal ;
now ex r being object st
( r > 0 & Ball (x,r) c= si ` )
x is
Element of
(TOP-REAL 1)
by EUCLID:67;
then
x is
Element of
REAL 1
by EUCLID:22;
then
x in REAL 1
;
then
x in 1
-tuples_on REAL
by EUCLID:def 1;
then
g in Funcs (
(Seg 1),
REAL)
by A25, FINSEQ_2:93;
then consider h being
Function such that A44:
g = h
and A45:
dom h = Seg 1
and A46:
rng h c= REAL
by FUNCT_2:def 2;
1
in Seg 1
by TARSKI:def 1, FINSEQ_1:2;
then
h . 1
in REAL
by A45, A46, FUNCT_1:3;
then reconsider g1 =
g1 as
Real by A44;
set r =
|.(g1 - (b . i)).|;
take r =
|.(g1 - (b . i)).|;
( r > 0 & Ball (x,r) c= si ` )
g1 - (b . i) <> 0
by A43, XXREAL_1:235;
hence
r > 0
;
Ball (x,r) c= si ` thus
Ball (
x,
r)
c= si `
verumproof
let t be
object ;
TARSKI:def 3 ( not t in Ball (x,r) or t in si ` )
assume A46bis:
t in Ball (
x,
r)
;
t in si `
then reconsider t1 =
t as
Element of
(Euclid 1) ;
(
t1 in Euclid 1 &
x in Euclid 1 )
;
then
(
t1 in TOP-REAL 1 &
x in TOP-REAL 1 )
by EUCLID:67;
then reconsider rt1 =
t1,
rx =
x as
Element of
REAL 1
by EUCLID:22;
Euclid 1
= MetrStruct(#
(REAL 1),
(Pitag_dist 1) #)
by EUCLID:def 7;
then A46ter:
dist (
x,
t1)
= |.(rx - rt1).|
by EUCLID:def 6;
now ex rt1 being Element of REAL 1 st
( t = rt1 & dom rt1 = dom <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> & ( for j being object st j in dom <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> holds
rt1 . j in <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> . j ) )take rt1 =
rt1;
( t = rt1 & dom rt1 = dom <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> & ( for j being object st j in dom <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> holds
rt1 . j in <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> . j ) )thus
t = rt1
;
( dom rt1 = dom <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> & ( for j being object st j in dom <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> holds
rt1 . j in <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> . j ) )
rt1 in REAL 1
;
then
rt1 in 1
-tuples_on REAL
by EUCLID:def 1;
then
rt1 in Funcs (
(Seg 1),
REAL)
by FINSEQ_2:93;
then consider h being
Function such that A47:
rt1 = h
and A48:
dom h = Seg 1
and
rng h c= REAL
by FUNCT_2:def 2;
thus
dom rt1 = dom <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*>
by A47, A48, FINSEQ_1:def 8;
for j being object st j in dom <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> holds
rt1 . j in <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> . jhereby verum
let j be
object ;
( j in dom <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> implies rt1 . j in <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> . j )assume
j in dom <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*>
;
rt1 . j in <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> . jthen A49:
j in {1}
by FINSEQ_1:2, FINSEQ_1:def 8;
then A50:
j = 1
by TARSKI:def 1;
consider rt2 being
Real such that A51:
rt1 = <*rt2*>
by Th6;
A52:
rt1 . j =
rt1 . 1
by A49, TARSKI:def 1
.=
rt2
by A51, FINSEQ_1:def 8
;
consider ux being
Real such that A53:
rx = <*ux*>
by Th6;
(
rx = 1
|-> ux &
rt1 = 1
|-> rt2 )
by A51, A53, FINSEQ_2:59;
then A54:
|.(rx - rt1).| =
(sqrt 1) * |.(ux - rt2).|
by TOPREALC:11
.=
|.(ux - rt2).|
by SQUARE_1:18
;
rt2 in ].-infty,(a . i).[ \/ ].(b . i),+infty.[
proof
ux = g1
by A25, A53, FINSEQ_1:def 8;
then A55:
|.(g1 - rt2).| < |.(g1 - (b . i)).|
by A54, A46bis, A46ter, METRIC_1:11;
0 < g1 - (b . i)
by A43, XXREAL_1:235, XREAL_1:50;
then A56:
|.(g1 - rt2).| < g1 - (b . i)
by A55, ABSVALUE:def 1;
g1 - rt2 < g1 - (b . i)
by A56, ABSVALUE:def 1;
then
(g1 - rt2) - g1 < (g1 - (b . i)) - g1
by XREAL_1:14;
then
- rt2 < - (b . i)
;
then
(
rt2 in ].-infty,(a . i).[ or
rt2 in ].(b . i),+infty.[ )
by XREAL_1:24, XXREAL_1:235;
hence
rt2 in ].-infty,(a . i).[ \/ ].(b . i),+infty.[
by XBOOLE_0:def 3;
verum
end; hence
rt1 . j in <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> . j
by A52, A50, FINSEQ_1:def 8;
verum
end; end;
hence
t in si `
by A23, CARD_3:def 5;
verum
end; end; hence
ex
r being
Real st
(
r > 0 &
Ball (
x,
r)
c= si ` )
;
verum end; end;
end;
hence
si ` in Family_open_set (Euclid 1)
by PCOMPS_1:def 4;
verum
end;
hence
si ` is
open
by COMPL_SP:def 3;
verum
end;
hence
s . i is
closed
by A22, COMPL_SP:def 4;
verum
end;
hence
s is
closed
by COMPL_SP:def 8;
verum
end;
hence
IntervalSequence (a,b) is non-empty pointwise_bounded closed SetSequence of (Euclid 1)
by A2, A7; verum