let T be non empty SubSpace of TOP-REAL n; :: thesis: ( T is convex implies T is arcwise_connected )
assume A1:
[#] T is convex Subset of (TOP-REAL n)
; :: according to TOPALG_2:def 1 :: thesis: T is arcwise_connected
let a, b be Point of T; :: according to BORSUK_2:def 3 :: thesis: a,b are_connected
A2:
( a in the carrier of T & b in the carrier of T )
;
the carrier of T is Subset of (TOP-REAL n)
by TSEP_1:1;
then reconsider a1 = a, b1 = b as Point of (TOP-REAL n) by A2;
per cases
( a1 <> b1 or a1 = b1 )
;
suppose
a1 <> b1
;
:: thesis: a,b are_connected then
LSeg a1,
b1 is_an_arc_of a1,
b1
by TOPREAL1:15;
then consider h being
Function of
I[01] ,
((TOP-REAL n) | (LSeg a1,b1)) such that A3:
h is
being_homeomorphism
and A4:
(
h . 0 = a1 &
h . 1
= b1 )
by TOPREAL1:def 2;
A5:
h is
continuous
by A3, TOPS_2:def 5;
[#] ((TOP-REAL n) | (LSeg a1,b1)) = LSeg a1,
b1
by PRE_TOPC:def 10;
then A6:
the
carrier of
((TOP-REAL n) | (LSeg a1,b1)) c= the
carrier of
T
by A1, JORDAN1:def 1;
then reconsider f =
h as
Function of
I[01] ,
T by FUNCT_2:9;
take
f
;
:: according to BORSUK_2:def 1 :: thesis: ( f is continuous & f . 0 = a & f . 1 = b )
(TOP-REAL n) | (LSeg a1,b1) is
SubSpace of
T
by A6, TSEP_1:4;
hence
f is
continuous
by A5, PRE_TOPC:56;
:: thesis: ( f . 0 = a & f . 1 = b )thus
(
f . 0 = a &
f . 1
= b )
by A4;
:: thesis: verum end;