let a, b be Real; :: thesis: for S being Subset of (Euclid 1) st a <= b & S = product <*[.a,b.]*> holds
S is bounded
let S be Subset of (Euclid 1); :: thesis: ( a <= b & S = product <*[.a,b.]*> implies S is bounded )
assume that
A1: a <= b and
A2: S = product <*[.a,b.]*> ; :: thesis: S is bounded
set si = product <*[.a,b.]*>;
reconsider si = product <*[.a,b.]*> as Subset of (Euclid 1) by A2;
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 - a;
per cases ( b - a = 0 or 0 < b - a ) by A1, XREAL_1:48;
suppose b - a = 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 A3: product <*[.a,b.]*> = product <*{a}*> by XXREAL_1:17
.= {<*a*>} 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 ) )
set r = 1;
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 A4: ( x = <*a*> & y = <*a*> ) by A3, TARSKI:def 1;
Euclid 1 is Reflexive ;
hence dist (x,y) <= r by A4, 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 A5: 0 < b - a ; :: 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 - a ; :: thesis: ( 0 < b - a & ( for x, y being Point of (Euclid 1) st x in si & y in si holds
dist (x,y) <= b - a ) )
thus 0 < b - a by A5; :: thesis: for x, y being Point of (Euclid 1) st x in si & y in si holds
dist (x,y) <= b - a
hereby :: thesis: verum
let x, y be Point of (Euclid 1); :: thesis: ( x in si & y in si implies dist (x,y) <= b - a )
assume that
A6: x in si and
A7: y in si ; :: thesis: dist (x,y) <= b - a
consider gx being Function such that
A8: x = gx and
dom gx = dom <*[.a,b.]*> and
A9: for j being object st j in dom <*[.a,b.]*> holds
gx . j in <*[.a,b.]*> . j by A6, CARD_3:def 5;
consider gy being Function such that
A10: y = gy and
dom gy = dom <*[.a,b.]*> and
A11: for j being object st j in dom <*[.a,b.]*> holds
gy . j in <*[.a,b.]*> . j by A7, 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 A12: dist (x,y) = |.(rx - ry).| by EUCLID:def 6;
consider ux being Real such that
A13: rx = <*ux*> by Th6;
consider uy being Real such that
A14: ry = <*uy*> by Th6;
( rx = 1 |-> ux & ry = 1 |-> uy ) by A13, A14, FINSEQ_2:59;
then A15: |.(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,b.]*> by FINSEQ_1:def 8;
then ( gx . 1 in <*[.a,b.]*> . 1 & gy . 1 in <*[.a,b.]*> . 1 ) by A9, A11;
then ( gx . 1 in [.a,b.] & gy . 1 in [.a,b.] ) by FINSEQ_1:def 8;
then ( ux in [.a,b.] & uy in [.a,b.] ) by A8, A10, A13, A14, FINSEQ_1:def 8;
hence dist (x,y) <= b - a by UNIFORM1:12, A15, A12; :: thesis: verum
end;
end;
end;
end;
hence S is bounded by A2; :: thesis: verum