let n be Element of NAT ; :: thesis: for A being Subset of (TOP-REAL n) holds
( A is Bounded iff ex r being Real st
for q being Point of (TOP-REAL n) st q in A holds
|.q.| < r )
let A be Subset of (TOP-REAL n); :: thesis: ( A is Bounded iff ex r being Real st
for q being Point of (TOP-REAL n) st q in A holds
|.q.| < r )
hereby :: thesis: ( ex r being Real st
for q being Point of (TOP-REAL n) st q in A holds
|.q.| < r implies A is Bounded )
assume A is Bounded ; :: thesis: ex r2 being Real st
for q being Point of (TOP-REAL n) st q in A holds
|.q.| < r2
then reconsider C = A as bounded Subset of (Euclid n) by Def2;
per cases ( C <> {} or C = {} ) ;
suppose A1: C <> {} ; :: thesis: ex r2 being Real st
for q being Point of (TOP-REAL n) st q in A holds
|.q.| < r2
consider x0 being Element of C;
x0 in C by A1;
then reconsider x0 = x0 as Point of (Euclid n) ;
consider r being Real such that
A2: ( 0 < r & ( for x, y being Point of (Euclid n) st x in C & y in C holds
dist x,y <= r ) ) by TBSP_1:def 9;
reconsider o = 0.REAL n as Point of (Euclid n) ;
set R0 = (r + (dist o,x0)) + 1;
for q being Point of (TOP-REAL n) st q in A holds
|.q.| < (r + (dist o,x0)) + 1
proof
let q1 be Point of (TOP-REAL n); :: thesis: ( q1 in A implies |.q1.| < (r + (dist o,x0)) + 1 )
assume A3: q1 in A ; :: thesis: |.q1.| < (r + (dist o,x0)) + 1
reconsider z = q1 as Point of (Euclid n) by TOPREAL3:13;
|.(q1 - (0.REAL n)).| = dist o,z by JGRAPH_1:45;
then A4: |.q1.| = dist o,z by Th13;
A5: dist x0,z <= r by A2, A3;
A6: dist o,z <= (dist o,x0) + (dist x0,z) by METRIC_1:4;
(dist o,x0) + (dist x0,z) <= (dist o,x0) + r by A5, XREAL_1:8;
then A7: dist o,z <= (dist o,x0) + r by A6, XXREAL_0:2;
r + (dist o,x0) < (r + (dist o,x0)) + 1 by XREAL_1:31;
hence |.q1.| < (r + (dist o,x0)) + 1 by A4, A7, XXREAL_0:2; :: thesis: verum
end;
hence ex r2 being Real st
for q being Point of (TOP-REAL n) st q in A holds
|.q.| < r2 ; :: thesis: verum
end;
suppose C = {} ; :: thesis: ex r2 being Real st
for q being Point of (TOP-REAL n) st q in A holds
|.q.| < r2
then for q being Point of (TOP-REAL n) st q in A holds
|.q.| < 1 ;
hence ex r2 being Real st
for q being Point of (TOP-REAL n) st q in A holds
|.q.| < r2 ; :: thesis: verum
end;
end;
end;
given r being Real such that A8: for q being Point of (TOP-REAL n) st q in A holds
|.q.| < r ; :: thesis: A is Bounded
reconsider C = A as Subset of (Euclid n) by TOPREAL3:13;
now
per cases ( C <> {} or C = {} ) ;
suppose A9: C <> {} ; :: thesis: C is bounded
consider x0 being Element of C;
x0 in C by A9;
then reconsider x0 = x0 as Point of (Euclid n) ;
reconsider q0 = x0 as Point of (TOP-REAL n) by TOPREAL3:13;
A10: |.q0.| < r by A8, A9;
reconsider o = 0.REAL n as Point of (Euclid n) ;
set R0 = r + r;
A11: 0 < r + r by A10;
for x, y being Point of (Euclid n) st x in C & y in C holds
dist x,y <= r + r
proof
let x, y be Point of (Euclid n); :: thesis: ( x in C & y in C implies dist x,y <= r + r )
assume A12: ( x in C & y in C ) ; :: thesis: dist x,y <= r + r
then reconsider q1 = x as Point of (TOP-REAL n) ;
reconsider q2 = y as Point of (TOP-REAL n) by A12;
A13: dist x,y <= (dist x,o) + (dist o,y) by METRIC_1:4;
dist x,o = |.(q1 - (0.REAL n)).| by JGRAPH_1:45
.= |.q1.| by Th13 ;
then A14: dist x,o < r by A8, A12;
dist o,y = |.(q2 - (0.REAL n)).| by JGRAPH_1:45
.= |.q2.| by Th13 ;
then dist o,y < r by A8, A12;
then (dist x,o) + (dist o,y) <= r + r by A14, XREAL_1:9;
hence dist x,y <= r + r by A13, XXREAL_0:2; :: thesis: verum
end;
hence C is bounded by A11, TBSP_1:def 9; :: thesis: verum
end;
end;
end;
hence A is Bounded by Def2; :: thesis: verum