let T be non empty SubSpace of R^1 ; :: thesis: ( T is convex implies T is arcwise_connected )
assume A1:
T is convex
; :: thesis: T is arcwise_connected
let a, b be Point of T; :: according to BORSUK_2:def 3 :: thesis: a,b are_connected
per cases
( a <= b or b <= a )
;
suppose A2:
a <= b
;
:: thesis: a,b are_connected set f =
L[01] ((#) a,b),
(a,b (#) );
A3:
[.a,b.] c= the
carrier of
T
by A1, Th12;
set X =
Closed-Interval-TSpace a,
b;
the
carrier of
(Closed-Interval-TSpace a,b) = [.a,b.]
by A2, TOPMETR:25;
then reconsider f =
L[01] ((#) a,b),
(a,b (#) ) as
Function of
I[01] ,
T by A3, FUNCT_2:9, TOPMETR:27;
take
f
;
:: according to BORSUK_2:def 1 :: thesis: ( f is continuous & f . 0 = a & f . 1 = b )
the
carrier of
(Closed-Interval-TSpace a,b) is
Subset of
R^1
by TSEP_1:1;
then reconsider g =
f as
Function of
I[01] ,
R^1 by FUNCT_2:9, TOPMETR:27;
L[01] ((#) a,b),
(a,b (#) ) is
continuous
by A2, TREAL_1:11;
then
g is
continuous
by PRE_TOPC:56, TOPMETR:27;
hence
f is
continuous
by PRE_TOPC:57;
:: thesis: ( f . 0 = a & f . 1 = b )thus f . 0 =
f . ((#) 0 ,1)
by TREAL_1:def 1
.=
(#) a,
b
by A2, TREAL_1:12
.=
a
by A2, TREAL_1:def 1
;
:: thesis: f . 1 = bthus f . 1 =
f . (0 ,1 (#) )
by TREAL_1:def 2
.=
a,
b (#)
by A2, TREAL_1:12
.=
b
by A2, TREAL_1:def 2
;
:: thesis: verum end; suppose A4:
b <= a
;
:: thesis: a,b are_connected set f =
L[01] (b,a (#) ),
((#) b,a);
A5:
[.b,a.] c= the
carrier of
T
by A1, Th12;
set X =
Closed-Interval-TSpace b,
a;
the
carrier of
(Closed-Interval-TSpace b,a) = [.b,a.]
by A4, TOPMETR:25;
then reconsider f =
L[01] (b,a (#) ),
((#) b,a) as
Function of
I[01] ,
T by A5, FUNCT_2:9, TOPMETR:27;
take
f
;
:: according to BORSUK_2:def 1 :: thesis: ( f is continuous & f . 0 = a & f . 1 = b )
the
carrier of
(Closed-Interval-TSpace b,a) is
Subset of
R^1
by TSEP_1:1;
then reconsider g =
f as
Function of
I[01] ,
R^1 by FUNCT_2:9, TOPMETR:27;
L[01] (b,a (#) ),
((#) b,a) is
continuous
by A4, TREAL_1:11;
then
g is
continuous
by PRE_TOPC:56, TOPMETR:27;
hence
f is
continuous
by PRE_TOPC:57;
:: thesis: ( f . 0 = a & f . 1 = b )thus f . 0 =
f . ((#) 0 ,1)
by TREAL_1:def 1
.=
b,
a (#)
by A4, TREAL_1:12
.=
a
by A4, TREAL_1:def 2
;
:: thesis: f . 1 = bthus f . 1 =
f . (0 ,1 (#) )
by TREAL_1:def 2
.=
(#) b,
a
by A4, TREAL_1:12
.=
b
by A4, TREAL_1:def 1
;
:: thesis: verum end;