let n be Nat; for A being Subset of (TOP-REAL n) st A is bounded holds
BDD A is bounded
let A be Subset of (TOP-REAL n); ( A is bounded implies BDD A is bounded )
assume
A is bounded
; BDD A is bounded
then consider r being Real such that
A1:
for q being Point of (TOP-REAL n) st q in A holds
|.q.| < r
by Th21;
per cases
( n >= 1 or n < 1 )
;
suppose A2:
n >= 1
;
BDD A is bounded set a =
r;
reconsider P =
(REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < r } as
Subset of
(TOP-REAL n) by EUCLID:22;
A3:
P c= A `
then A5:
Down (
P,
(A `))
= P
by XBOOLE_1:28;
now BDD A is bounded per cases
( n >= 2 or n < 2 )
;
suppose
n >= 2
;
BDD A is bounded then A6:
P is
connected
by Th40;
now BDD A is bounded assume
not
BDD A is
bounded
;
contradictionthen consider q being
Point of
(TOP-REAL n) such that A7:
q in BDD A
and A8:
not
|.q.| < r
by Th21;
consider y being
set such that A9:
q in y
and A10:
y in { B3 where B3 is Subset of (TOP-REAL n) : B3 is_inside_component_of A }
by A7, TARSKI:def 4;
consider B3 being
Subset of
(TOP-REAL n) such that A11:
y = B3
and A12:
B3 is_inside_component_of A
by A10;
q in the
carrier of
(TOP-REAL n)
;
then A13:
q in REAL n
by EUCLID:22;
B3 is_a_component_of A `
by A12;
then consider B4 being
Subset of
((TOP-REAL n) | (A `)) such that A14:
B4 = B3
and A15:
B4 is
a_component
by CONNSP_1:def 6;
for
q2 being
Point of
(TOP-REAL n) st
q2 = q holds
|.q2.| >= r
by A8;
then
not
q in { q2 where q2 is Point of (TOP-REAL n) : |.q2.| < r }
;
then
q in P
by A13, XBOOLE_0:def 5;
then
P /\ B4 <> {} ((TOP-REAL n) | (A `))
by A9, A11, A14, XBOOLE_0:def 4;
then
P meets B4
;
then A16:
P c= B4
by A5, A6, A15, CONNSP_1:36, CONNSP_1:46;
B3 is
bounded
by A12;
hence
contradiction
by A2, A14, A16, Th41, RLTOPSP1:42;
verum end; hence
BDD A is
bounded
;
verum end; suppose A17:
n < 2
;
BDD A is bounded
{ q where q is Point of (TOP-REAL n) : for r2 being Real st q = |[r2]| holds
r2 >= r } c= the
carrier of
(TOP-REAL n)
then reconsider P2 =
{ q where q is Point of (TOP-REAL n) : for r2 being Real st q = |[r2]| holds
r2 >= r } as
Subset of
(TOP-REAL n) ;
{ q where q is Point of (TOP-REAL n) : for r2 being Real st q = |[r2]| holds
r2 <= - r } c= the
carrier of
(TOP-REAL n)
then reconsider P1 =
{ q where q is Point of (TOP-REAL n) : for r2 being Real st q = |[r2]| holds
r2 <= - r } as
Subset of
(TOP-REAL n) ;
n < 1
+ 1
by A17;
then
n <= 1
by NAT_1:13;
then A18:
n = 1
by A2, XXREAL_0:1;
A19:
P c= P1 \/ P2
P1 \/ P2 c= P
then A35:
P = P1 \/ P2
by A19;
then
P2 c= P
by XBOOLE_1:7;
then A36:
Down (
P2,
(A `))
= P2
by A3, XBOOLE_1:1, XBOOLE_1:28;
for
w1,
w2 being
Point of
(TOP-REAL n) st
w1 in P2 &
w2 in P2 holds
LSeg (
w1,
w2)
c= P2
then
P2 is
convex
by JORDAN1:def 1;
then A49:
Down (
P2,
(A `)) is
connected
by A36, CONNSP_1:46;
P1 c= P
by A35, XBOOLE_1:7;
then A50:
Down (
P1,
(A `))
= P1
by A3, XBOOLE_1:1, XBOOLE_1:28;
for
w1,
w2 being
Point of
(TOP-REAL n) st
w1 in P1 &
w2 in P1 holds
LSeg (
w1,
w2)
c= P1
then
P1 is
convex
by JORDAN1:def 1;
then A77:
Down (
P1,
(A `)) is
connected
by A50, CONNSP_1:46;
now BDD A is bounded assume
not
BDD A is
bounded
;
contradictionthen consider q being
Point of
(TOP-REAL n) such that A78:
q in BDD A
and A79:
not
|.q.| < r
by Th21;
consider y being
set such that A80:
q in y
and A81:
y in { B3 where B3 is Subset of (TOP-REAL n) : B3 is_inside_component_of A }
by A78, TARSKI:def 4;
consider B3 being
Subset of
(TOP-REAL n) such that A82:
y = B3
and A83:
B3 is_inside_component_of A
by A81;
q in the
carrier of
(TOP-REAL n)
;
then A84:
q in REAL n
by EUCLID:22;
for
q2 being
Point of
(TOP-REAL n) st
q2 = q holds
|.q2.| >= r
by A79;
then
not
q in { q2 where q2 is Point of (TOP-REAL n) : |.q2.| < r }
;
then A85:
q in P
by A84, XBOOLE_0:def 5;
B3 is_a_component_of A `
by A83;
then consider B4 being
Subset of
((TOP-REAL n) | (A `)) such that A86:
B4 = B3
and A87:
B4 is
a_component
by CONNSP_1:def 6;
per cases
( q in P1 or q in P2 )
by A19, A85, XBOOLE_0:def 3;
suppose
q in P1
;
contradictionthen
P1 /\ B4 <> {} ((TOP-REAL n) | (A `))
by A80, A82, A86, XBOOLE_0:def 4;
then A88:
P1 meets B4
;
B3 is
bounded
by A83;
hence
contradiction
by A50, A57, A77, A86, A87, A88, CONNSP_1:36, RLTOPSP1:42;
verum end; suppose
q in P2
;
contradictionthen
P2 /\ B4 <> {} ((TOP-REAL n) | (A `))
by A80, A82, A86, XBOOLE_0:def 4;
then A89:
P2 meets B4
;
B3 is
bounded
by A83;
hence
contradiction
by A36, A51, A49, A86, A87, A89, CONNSP_1:36, RLTOPSP1:42;
verum end; end; hence
BDD A is
bounded
;
verum end; hence
BDD A is
bounded
;
verum end;