let n be Nat; for A being Subset of (TOP-REAL n) st n >= 2 & A is bounded holds
UBD A is_outside_component_of A
let A be Subset of (TOP-REAL n); ( n >= 2 & A is bounded implies UBD A is_outside_component_of A )
assume that
A1:
n >= 2
and
A2:
A is bounded
; UBD A is_outside_component_of A
reconsider C = A as bounded Subset of (Euclid n) by A2, Th5;
per cases
( C <> {} or C = {} )
;
suppose A3:
C <> {}
;
UBD A is_outside_component_of Aset x0 = the
Element of
C;
A4:
the
Element of
C in C
by A3;
then reconsider q1 = the
Element of
C as
Point of
(TOP-REAL n) ;
reconsider o =
0. (TOP-REAL n) as
Point of
(Euclid n) by EUCLID:67;
reconsider x0 = the
Element of
C as
Point of
(Euclid n) by A4;
consider r being
Real such that
0 < r
and A5:
for
x,
y being
Point of
(Euclid n) st
x in C &
y in C holds
dist (
x,
y)
<= r
by TBSP_1:def 7;
set R0 =
(r + (dist (o,x0))) + 1;
reconsider W =
(REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < (r + (dist (o,x0))) + 1 } as
Subset of
(Euclid n) ;
A6:
now not W meets Aassume
W meets A
;
contradictionthen consider z being
object such that A7:
z in W
and A8:
z in A
by XBOOLE_0:3;
A9:
not
z in { q where q is Point of (TOP-REAL n) : |.q.| < (r + (dist (o,x0))) + 1 }
by A7, XBOOLE_0:def 5;
reconsider z =
z as
Point of
(Euclid n) by A7;
dist (
x0,
z)
<= r
by A5, A8;
then
(
dist (
o,
z)
<= (dist (o,x0)) + (dist (x0,z)) &
(dist (o,x0)) + (dist (x0,z)) <= (dist (o,x0)) + r )
by METRIC_1:4, XREAL_1:6;
then A10:
dist (
o,
z)
<= (dist (o,x0)) + r
by XXREAL_0:2;
reconsider q1 =
z as
Point of
(TOP-REAL n) by TOPREAL3:8;
A11:
|.(q1 - (0. (TOP-REAL n))).| = dist (
o,
z)
by JGRAPH_1:28;
|.q1.| >= (r + (dist (o,x0))) + 1
by A9;
then
dist (
o,
z)
>= (r + (dist (o,x0))) + 1
by A11, RLVECT_1:13;
then
r + ((dist (o,x0)) + 1) <= r + (dist (o,x0))
by A10, XXREAL_0:2;
then
(dist (o,x0)) + 1
<= (dist (o,x0)) + 0
by XREAL_1:6;
hence
contradiction
by XREAL_1:6;
verum end; reconsider P =
W as
Subset of
(TOP-REAL n) by TOPREAL3:8;
reconsider P =
P as
Subset of
(TOP-REAL n) ;
the
carrier of
((TOP-REAL n) | (A `)) = A `
by PRE_TOPC:8;
then reconsider P1 =
Component_of (Down (P,(A `))) as
Subset of
(TOP-REAL n) by XBOOLE_1:1;
A12:
P is
connected
by A1, Th40;
A13:
UBD A c= P1
proof
A14:
(TOP-REAL n) | P is
connected
by A12, CONNSP_1:def 3;
A15:
P c= A `
by A6, SUBSET_1:23;
then
Down (
P,
(A `))
= P
by XBOOLE_1:28;
then
((TOP-REAL n) | (A `)) | (Down (P,(A `))) is
connected
by A15, A14, PRE_TOPC:7;
then A16:
Down (
P,
(A `)) is
connected
by CONNSP_1:def 3;
reconsider G =
A ` as non
empty Subset of
(TOP-REAL n) by A1, A2, Th51, XXREAL_0:2;
let z be
object ;
TARSKI:def 3 ( not z in UBD A or z in P1 )
assume
z in UBD A
;
z in P1
then consider y being
set such that A17:
z in y
and A18:
y in { B where B is Subset of (TOP-REAL n) : B is_outside_component_of A }
by TARSKI:def 4;
consider B being
Subset of
(TOP-REAL n) such that A19:
y = B
and A20:
B is_outside_component_of A
by A18;
consider C2 being
Subset of
((TOP-REAL n) | (A `)) such that A21:
C2 = B
and A22:
C2 is
a_component
and A23:
C2 is not
bounded Subset of
(Euclid n)
by A20, Th8;
consider D2 being
Subset of
(Euclid n) such that A24:
D2 = { q where q is Point of (TOP-REAL n) : |.q.| < (r + (dist (o,x0))) + 1 }
by Th52;
reconsider D2 =
D2 as
Subset of
(Euclid n) ;
A25:
A c= D2
proof
let z be
object ;
TARSKI:def 3 ( not z in A or z in D2 )
A26:
|.q1.| =
|.(q1 - (0. (TOP-REAL n))).|
by RLVECT_1:13
.=
dist (
x0,
o)
by JGRAPH_1:28
;
assume A27:
z in A
;
z in D2
then reconsider q2 =
z as
Point of
(TOP-REAL n) ;
reconsider x1 =
q2 as
Point of
(Euclid n) by TOPREAL3:8;
(
|.(q2 - q1).| = dist (
x1,
x0) &
dist (
x1,
x0)
<= r )
by A5, A27, JGRAPH_1:28;
then A28:
|.(q2 - q1).| + |.q1.| <= r + (dist (o,x0))
by A26, XREAL_1:6;
A29:
r + (dist (o,x0)) < (r + (dist (o,x0))) + 1
by XREAL_1:29;
(
|.q2.| = |.((q2 - q1) + q1).| &
|.((q2 - q1) + q1).| <= |.(q2 - q1).| + |.q1.| )
by RLVECT_4:1, TOPRNS_1:29;
then
|.q2.| <= r + (dist (o,x0))
by A28, XXREAL_0:2;
then
|.q2.| < (r + (dist (o,x0))) + 1
by A29, XXREAL_0:2;
hence
z in D2
by A24;
verum
end;
the
carrier of
(Euclid n) = the
carrier of
(TOP-REAL n)
by TOPREAL3:8;
then
D2 ` c= the
carrier of
(TOP-REAL n) \ A
by A25, XBOOLE_1:34;
then A30:
P /\ (D2 `) c= P /\ (A `)
by XBOOLE_1:26;
then
(Down (P,(A `))) /\ C2 <> {}
by A24, A30, XBOOLE_1:3, XBOOLE_1:26;
then A34:
Down (
P,
(A `))
meets C2
;
C2 is
connected
by A22, CONNSP_1:def 5;
then
C2 c= Component_of (Down (P,(A `)))
by A16, A34, CONNSP_3:16;
hence
z in P1
by A17, A19, A21;
verum
end;
not
W is
bounded
by A1, Th47;
then
(
P1 is_outside_component_of A &
P1 c= UBD A )
by A12, A6, Th14, Th48;
hence
UBD A is_outside_component_of A
by A13, XBOOLE_0:def 10;
verum end; suppose A35:
C = {}
;
UBD A is_outside_component_of A
REAL n c= the
carrier of
(Euclid n)
;
then reconsider W =
REAL n as
Subset of
(Euclid n) ;
W /\ A = {}
by A35;
then A36:
W misses A
;
reconsider P =
W as
Subset of
(TOP-REAL n) by TOPREAL3:8;
reconsider P =
P as
Subset of
(TOP-REAL n) ;
the
carrier of
((TOP-REAL n) | (A `)) = A `
by PRE_TOPC:8;
then reconsider P1 =
Component_of (Down (P,(A `))) as
Subset of
(TOP-REAL n) by XBOOLE_1:1;
[#] (TOP-REAL n) is
a_component
;
then A37:
[#] TopStruct(# the
carrier of
(TOP-REAL n), the
topology of
(TOP-REAL n) #) is
a_component
by CONNSP_1:45;
not
W is
bounded
by A1, Th20, XXREAL_0:2;
then A38:
P1 is_outside_component_of A
by A36, Th19, Th48;
A = {} (TOP-REAL n)
by A35;
then A39:
UBD A = REAL n
by A1, Th23, XXREAL_0:2;
(
[#] (TOP-REAL n) = REAL n &
(TOP-REAL n) | ([#] (TOP-REAL n)) = TopStruct(# the
carrier of
(TOP-REAL n), the
topology of
(TOP-REAL n) #) )
by EUCLID:22, TSEP_1:93;
hence
UBD A is_outside_component_of A
by A35, A38, A39, A37, CONNSP_3:7;
verum end;