let M be non empty MetrSpace; for A being Subset of M
for B being non empty Subset of M
for C being Subset of (M | B) st A = C & C is bounded holds
A is bounded
let A be Subset of M; for B being non empty Subset of M
for C being Subset of (M | B) st A = C & C is bounded holds
A is bounded
let B be non empty Subset of M; for C being Subset of (M | B) st A = C & C is bounded holds
A is bounded
let C be Subset of (M | B); ( A = C & C is bounded implies A is bounded )
assume that
A1:
A = C
and
A2:
C is bounded
; A is bounded
consider r0 being Real such that
A3:
0 < r0
and
A4:
for x, y being Point of (M | B) st x in C & y in C holds
dist (x,y) <= r0
by A2, TBSP_1:def 7;
for x, y being Point of M st x in A & y in A holds
dist (x,y) <= r0
proof
let x,
y be
Point of
M;
( x in A & y in A implies dist (x,y) <= r0 )
assume A5:
(
x in A &
y in A )
;
dist (x,y) <= r0
then reconsider x0 =
x,
y0 =
y as
Point of
(M | B) by A1;
A6:
( the
distance of
(M | B) . (
x0,
y0)
= the
distance of
M . (
x,
y) & the
distance of
(M | B) . (
x0,
y0)
= dist (
x0,
y0) )
by METRIC_1:def 1, TOPMETR:def 1;
dist (
x0,
y0)
<= r0
by A1, A4, A5;
hence
dist (
x,
y)
<= r0
by A6, METRIC_1:def 1;
verum
end;
hence
A is bounded
by A3, TBSP_1:def 7; verum