let n be Element of 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, Def2;
per cases
( C <> {} or C = {} )
;
suppose A3:
C <> {}
;
UBD A is_outside_component_of Aconsider x0 being
Element of
C;
A4:
x0 in C
by A3;
then reconsider q1 =
x0 as
Point of
(TOP-REAL n) ;
reconsider o =
0. (TOP-REAL n) as
Point of
(Euclid n) by EUCLID:71;
reconsider x0 =
x0 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 9;
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 assume
W meets A
;
contradictionthen consider z being
set 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:8;
then A10:
dist o,
z <= (dist o,x0) + r
by XXREAL_0:2;
reconsider q1 =
z as
Point of
(TOP-REAL n) by TOPREAL3:13;
A11:
|.(q1 - (0. (TOP-REAL n))).| = dist o,
z
by JGRAPH_1:45;
|.q1.| >= (r + (dist o,x0)) + 1
by A9;
then
dist o,
z >= (r + (dist o,x0)) + 1
by A11, RLVECT_1:26;
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:8;
hence
contradiction
by XREAL_1:8;
verum end; reconsider P =
W as
Subset of
(TOP-REAL n) by TOPREAL3:13;
reconsider P =
P as
Subset of
(TOP-REAL n) ;
the
carrier of
((TOP-REAL n) | (A ` )) = A `
by PRE_TOPC:29;
then reconsider P1 =
Component_of (Down P,(A ` )) as
Subset of
(TOP-REAL n) by XBOOLE_1:1;
A12:
P is
connected
by A1, Th70;
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:43;
then
Down P,
(A ` ) = P
by XBOOLE_1:28;
then
((TOP-REAL n) | (A ` )) | (Down P,(A ` )) is
connected
by A15, A14, PRE_TOPC:28;
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, Th74, XXREAL_0:2;
let z be
set ;
TARSKI:def 3 ( not z in UBD A or z in P1 )
A17:
(TOP-REAL n) | G is non
empty TopSpace
;
assume
z in UBD A
;
z in P1
then consider y being
set such that A18:
z in y
and A19:
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 A20:
y = B
and A21:
B is_outside_component_of A
by A19;
consider C2 being
Subset of
((TOP-REAL n) | (A ` )) such that A22:
C2 = B
and A23:
C2 is_a_component_of (TOP-REAL n) | (A ` )
and A24:
C2 is not
bounded Subset of
(Euclid n)
by A21, Th18;
consider D2 being
Subset of
(Euclid n) such that A25:
D2 = { q where q is Point of (TOP-REAL n) : |.q.| < (r + (dist o,x0)) + 1 }
by Th75;
reconsider D2 =
D2 as
Subset of
(Euclid n) ;
A26:
A c= D2
proof
let z be
set ;
TARSKI:def 3 ( not z in A or z in D2 )
A27:
|.q1.| =
|.(q1 - (0. (TOP-REAL n))).|
by RLVECT_1:26
.=
dist x0,
o
by JGRAPH_1:45
;
assume A28:
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:13;
(
|.(q2 - q1).| = dist x1,
x0 &
dist x1,
x0 <= r )
by A5, A28, JGRAPH_1:45;
then A29:
|.(q2 - q1).| + |.q1.| <= r + (dist o,x0)
by A27, XREAL_1:8;
A30:
r + (dist o,x0) < (r + (dist o,x0)) + 1
by XREAL_1:31;
(
|.q2.| = |.((q2 - q1) + q1).| &
|.((q2 - q1) + q1).| <= |.(q2 - q1).| + |.q1.| )
by EUCLID:52, TOPRNS_1:30;
then
|.q2.| <= r + (dist o,x0)
by A29, XXREAL_0:2;
then
|.q2.| < (r + (dist o,x0)) + 1
by A30, XXREAL_0:2;
hence
z in D2
by A25;
verum
end;
the
carrier of
(Euclid n) = the
carrier of
(TOP-REAL n)
by TOPREAL3:13;
then
D2 ` c= the
carrier of
(TOP-REAL n) \ A
by A26, XBOOLE_1:34;
then A31:
P /\ (D2 ` ) c= P /\ (A ` )
by XBOOLE_1:26;
then
(Down P,(A ` )) /\ C2 <> {}
by A25, A31, XBOOLE_1:3, XBOOLE_1:26;
then A35:
Down P,
(A ` ) meets C2
by XBOOLE_0:def 7;
C2 is
connected
by A23, CONNSP_1:def 5;
then
C2 c= Component_of (Down P,(A ` ))
by A16, A35, A17, CONNSP_3:16;
hence
z in P1
by A18, A20, A22;
verum
end;
P = W
;
then
not
W is
bounded
by A1, Th70;
then
(
P1 is_outside_component_of A &
P1 c= UBD A )
by A12, A6, Th27, Th71;
hence
UBD A is_outside_component_of A
by A13, XBOOLE_0:def 10;
verum end; suppose A36:
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 A36;
then A37:
W misses A
by XBOOLE_0:def 7;
reconsider P =
W as
Subset of
(TOP-REAL n) by TOPREAL3:13;
reconsider P =
P as
Subset of
(TOP-REAL n) ;
the
carrier of
((TOP-REAL n) | (A ` )) = A `
by PRE_TOPC:29;
then reconsider P1 =
Component_of (Down P,(A ` )) as
Subset of
(TOP-REAL n) by XBOOLE_1:1;
[#] (TOP-REAL n) is_a_component_of TOP-REAL n
by Th23;
then A38:
[#] TopStruct(# the
carrier of
(TOP-REAL n),the
topology of
(TOP-REAL n) #)
is_a_component_of TopStruct(# the
carrier of
(TOP-REAL n),the
topology of
(TOP-REAL n) #)
by CONNSP_1:48;
not
W is
bounded
by A1, Th39, XXREAL_0:2;
then A39:
P1 is_outside_component_of A
by A37, Th33, Th71;
A = {} (TOP-REAL n)
by A36;
then A40:
UBD A = REAL n
by A1, Th42, 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:25, TSEP_1:100;
hence
UBD A is_outside_component_of A
by A36, A39, A40, A38, CONNSP_3:7;
verum end;