let M be non empty MetrSpace; :: thesis: for B being Subset of M
for A being Subset of (TopSpaceMetr M) st A = B & A is compact holds
B is bounded
let B be Subset of M; :: thesis: for A being Subset of (TopSpaceMetr M) st A = B & A is compact holds
B is bounded
let A be Subset of (TopSpaceMetr M); :: thesis: ( A = B & A is compact implies B is bounded )
set TA = TopSpaceMetr M;
assume that
A1: A = B and
A2: A is compact ; :: thesis: B is bounded
A c= the carrier of ((TopSpaceMetr M) | A) by PRE_TOPC:8;
then reconsider A2 = A as Subset of ((TopSpaceMetr M) | A) ;
per cases ( A <> {} or A = {} ) ;
suppose A <> {} ; :: thesis: B is bounded
then reconsider A1 = A as non empty Subset of M by TOPMETR:12;
[#] ((TopSpaceMetr M) | A) = A2 by PRE_TOPC:def 5;
then [#] ((TopSpaceMetr M) | A) is compact by A2, COMPTS_1:2;
then A3: (TopSpaceMetr M) | A is compact by COMPTS_1:1;
TopSpaceMetr (M | A1) = (TopSpaceMetr M) | A by Th16;
then M | A1 is totally_bounded by A3, TBSP_1:9;
then M | A1 is bounded by TBSP_1:19;
then A4: [#] (M | A1) is bounded ;
[#] (M | A1) = the carrier of (M | A1)
.= A1 by TOPMETR:def 2 ;
hence B is bounded by A1, A4, Th17; :: thesis: verum
end;
suppose A = {} ; :: thesis: B is bounded
then A = {} M ;
hence B is bounded by A1; :: thesis: verum
end;
end;