let n be Element of NAT ; :: thesis: for P being Subset of (TOP-REAL n) st P is convex holds
P is connected
let P be Subset of (TOP-REAL n); :: thesis: ( P is convex implies P is connected )
assume A1:
for w3, w4 being Point of (TOP-REAL n) st w3 in P & w4 in P holds
LSeg w3,w4 c= P
; :: according to JORDAN1:def 1 :: thesis: P is connected
for w1, w2 being Point of (TOP-REAL n) st w1 in P & w2 in P & w1 <> w2 holds
ex h being Function of I[01] ,((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w2 = h . 1 )
proof
let w1,
w2 be
Point of
(TOP-REAL n);
:: thesis: ( w1 in P & w2 in P & w1 <> w2 implies ex h being Function of I[01] ,((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w2 = h . 1 ) )
assume A2:
(
w1 in P &
w2 in P &
w1 <> w2 )
;
:: thesis: ex h being Function of I[01] ,((TOP-REAL n) | P) st
( h is continuous & w1 = h . 0 & w2 = h . 1 )
then A3:
LSeg w1,
w2 c= P
by A1;
LSeg w1,
w2 is_an_arc_of w1,
w2
by A2, TOPREAL1:15;
then consider f being
Function of
I[01] ,
((TOP-REAL n) | (LSeg w1,w2)) such that A4:
(
f is
being_homeomorphism &
f . 0 = w1 &
f . 1
= w2 )
by TOPREAL1:def 2;
A5:
f is
continuous
by A4, TOPS_2:def 5;
A6:
rng f = [#] ((TOP-REAL n) | (LSeg w1,w2))
by A4, TOPS_2:def 5;
then A7:
rng f c= P
by A3, PRE_TOPC:def 10;
then
[#] ((TOP-REAL n) | (LSeg w1,w2)) c= [#] ((TOP-REAL n) | P)
by A6, PRE_TOPC:def 10;
then A8:
(TOP-REAL n) | (LSeg w1,w2) is
SubSpace of
(TOP-REAL n) | P
by TOPMETR:4;
not
LSeg w1,
w2 is
empty
;
then
not
(TOP-REAL n) | (LSeg w1,w2) is
empty
;
then X:
the
carrier of
((TOP-REAL n) | (LSeg w1,w2)) <> {}
;
the
carrier of
I[01] = [.0 ,1.]
by BORSUK_1:83;
then
dom f = [.0 ,1.]
by FUNCT_2:def 1, X;
then reconsider g =
f as
Function of
[.0 ,1.],
P by A7, FUNCT_2:4;
the
carrier of
((TOP-REAL n) | P) =
[#] ((TOP-REAL n) | P)
.=
P
by PRE_TOPC:def 10
;
then reconsider gt =
g as
Function of
I[01] ,
((TOP-REAL n) | P) by BORSUK_1:83;
gt is
continuous
by A5, A8, PRE_TOPC:56;
hence
ex
h being
Function of
I[01] ,
((TOP-REAL n) | P) st
(
h is
continuous &
w1 = h . 0 &
w2 = h . 1 )
by A4;
:: thesis: verum
end;
hence
P is connected
by Th5; :: thesis: verum