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