let a, b be Real_Sequence; :: thesis: ( ( 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 ) ; :: thesis: 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 ; :: thesis: 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; :: thesis: verum
end;
A7: s is pointwise_bounded
proof
now :: thesis: for i being Nat holds s . i is bounded
let i be Nat; :: thesis: 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 (b . i) - (a . i) = 0 ; :: thesis: 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 ) )
then A9: product <*[.(a . i),(b . i).]*> = product <*{(a . i)}*> by XXREAL_1:17
.= {<*(a . i)*>} by Th5 ;
now :: thesis: ex r being Element of NAT st
( 0 < r & ( for x, y being Point of (Euclid 1) st x in si & y in si holds
dist (x,y) <= r ) )
take r = 1; :: thesis: ( 0 < r & ( for x, y being Point of (Euclid 1) st x in si & y in si holds
dist (x,y) <= r ) )
thus 0 < r ; :: thesis: for x, y being Point of (Euclid 1) st x in si & y in si holds
dist (x,y) <= r
hereby :: thesis: verum
let x, y be Point of (Euclid 1); :: thesis: ( x in si & y in si implies dist (x,y) <= r )
assume ( x in si & y in si ) ; :: thesis: dist (x,y) <= r
then A10: ( x = <*(a . i)*> & y = <*(a . i)*> ) by A9, TARSKI:def 1;
Euclid 1 is Reflexive ;
hence dist (x,y) <= r by A10, METRIC_1:def 2; :: thesis: verum
end;
end;
hence 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 ) ) ; :: thesis: verum
end;
suppose A11: 0 < (b . i) - (a . i) ; :: thesis: 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) ; :: thesis: ( 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; :: thesis: for x, y being Point of (Euclid 1) st x in si & y in si holds
dist (x,y) <= (b . i) - (a . i)
hereby :: thesis: verum
let x, y be Point of (Euclid 1); :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum
end;
end;
end;
end;
then si is bounded ;
hence s . i is bounded by Def1; :: thesis: verum
end;
hence s is pointwise_bounded by COMPL_SP:def 1; :: thesis: verum
end;
s is closed
proof
for i being Nat holds s . i is closed
proof
let i be Nat; :: thesis: 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.[)*>
proof
si ` = the carrier of (TOP-REAL 1) \ si by EUCLID:67
.= (REAL 1) \ (product <*[.(a . i),(b . i).]*>) by EUCLID:22
.= product <*(REAL \ [.(a . i),(b . i).])*> by Th18, SRINGS_4:27 ;
hence si ` = product <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> by XXREAL_1:385; :: thesis: verum
end;
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); :: thesis: ( x in si ` implies ex r being Real st
( r > 0 & Ball (x,r) c= si ` ) )
assume A24: x in si ` ; :: thesis: 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).[ ; :: thesis: ex r being Real st
( r > 0 & Ball (x,r) c= si ` )
then reconsider g1 = g . 1 as ExtReal ;
now :: thesis: 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)).|; :: thesis: ( r > 0 & Ball (x,r) c= si ` )
g1 - (a . i) <> 0 by A27, XXREAL_1:233;
hence r > 0 ; :: thesis: Ball (x,r) c= si `
thus Ball (x,r) c= si ` :: thesis: verum
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in Ball (x,r) or t in si ` )
assume A31: t in Ball (x,r) ; :: thesis: 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 :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: 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
hereby :: thesis: verum
let j be object ; :: thesis: ( 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.[)*> ; :: thesis: rt1 . j in <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> . j
then 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.[
proof
A41: |.(ux - rt2).| < |.(g1 - (a . i)).| by A40, A32, A31, METRIC_1:11;
g1 - (a . i) < 0 by A27, XXREAL_1:233, XREAL_1:49;
then |.(g1 - (a . i)).| = - (g1 - (a . i)) by ABSVALUE:def 1;
then A42: |.(g1 - rt2).| < (a . i) - g1 by A25, A39, FINSEQ_1:def 8, A41;
per cases ( 0 <= g1 - rt2 or g1 - rt2 < 0 ) ;
suppose g1 - rt2 < 0 ; :: thesis: rt2 in ].-infty,(a . i).[ \/ ].(b . i),+infty.[
then - (g1 - rt2) < (a . i) - g1 by A42, ABSVALUE:def 1;
then (rt2 - g1) + g1 < ((a . i) - g1) + g1 by XREAL_1:8;
then ( rt2 in ].-infty,(a . i).[ or rt2 in ].(b . i),+infty.[ ) by XXREAL_1:233;
hence rt2 in ].-infty,(a . i).[ \/ ].(b . i),+infty.[ by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
hence rt1 . j in <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> . j by A36, FINSEQ_1:def 8, A38; :: thesis: verum
end;
end;
hence t in si ` by A23, CARD_3:def 5; :: thesis: verum
end;
end;
hence ex r being Real st
( r > 0 & Ball (x,r) c= si ` ) ; :: thesis: verum
end;
suppose A43: g . 1 in ].(b . i),+infty.[ ; :: thesis: ex r being Real st
( r > 0 & Ball (x,r) c= si ` )
then reconsider g1 = g . 1 as ExtReal ;
now :: thesis: 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)).|; :: thesis: ( r > 0 & Ball (x,r) c= si ` )
g1 - (b . i) <> 0 by A43, XXREAL_1:235;
hence r > 0 ; :: thesis: Ball (x,r) c= si `
thus Ball (x,r) c= si ` :: thesis: verum
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in Ball (x,r) or t in si ` )
assume A46bis: t in Ball (x,r) ; :: thesis: 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 :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: 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
hereby :: thesis: verum
let j be object ; :: thesis: ( 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.[)*> ; :: thesis: rt1 . j in <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> . j
then 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; :: thesis: verum
end;
hence rt1 . j in <*(].-infty,(a . i).[ \/ ].(b . i),+infty.[)*> . j by A52, A50, FINSEQ_1:def 8; :: thesis: verum
end;
end;
hence t in si ` by A23, CARD_3:def 5; :: thesis: verum
end;
end;
hence ex r being Real st
( r > 0 & Ball (x,r) c= si ` ) ; :: thesis: verum
end;
end;
end;
hence si ` in Family_open_set (Euclid 1) by PCOMPS_1:def 4; :: thesis: verum
end;
hence si ` is open by COMPL_SP:def 3; :: thesis: verum
end;
hence s . i is closed by A22, COMPL_SP:def 4; :: thesis: verum
end;
hence s is closed by COMPL_SP:def 8; :: thesis: verum
end;
hence IntervalSequence (a,b) is non-empty pointwise_bounded closed SetSequence of (Euclid 1) by A2, A7; :: thesis: verum