let T be non empty SubSpace of R^1 ; ( T is interval implies T is pathwise_connected )
assume A1:
T is interval
; T is pathwise_connected
let a, b be Point of T; BORSUK_2:def 3 a,b are_connected
per cases
( a <= b or b <= a )
;
suppose A2:
a <= b
;
a,b are_connected set f =
L[01] (
((#) (a,b)),
((a,b) (#)));
set X =
Closed-Interval-TSpace (
a,
b);
A3:
the
carrier of
(Closed-Interval-TSpace (a,b)) = [.a,b.]
by A2, TOPMETR:18;
[.a,b.] c= the
carrier of
T
by A1, Th8;
then reconsider f =
L[01] (
((#) (a,b)),
((a,b) (#))) as
Function of
I[01],
T by A3, FUNCT_2:7, TOPMETR:20;
take
f
;
BORSUK_2:def 1 ( 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:7, TOPMETR:20;
L[01] (
((#) (a,b)),
((a,b) (#))) is
continuous
by A2, TREAL_1:8;
then
g is
continuous
by PRE_TOPC:26, TOPMETR:20;
hence
f is
continuous
by PRE_TOPC:27;
( f . 0 = a & f . 1 = b )thus f . 0 =
f . ((#) (0,1))
by TREAL_1:def 1
.=
(#) (
a,
b)
by A2, TREAL_1:9
.=
a
by A2, TREAL_1:def 1
;
f . 1 = bthus f . 1 =
f . ((0,1) (#))
by TREAL_1:def 2
.=
(
a,
b)
(#)
by A2, TREAL_1:9
.=
b
by A2, TREAL_1:def 2
;
verum end; suppose A4:
b <= a
;
a,b are_connected set f =
L[01] (
((b,a) (#)),
((#) (b,a)));
set X =
Closed-Interval-TSpace (
b,
a);
A5:
the
carrier of
(Closed-Interval-TSpace (b,a)) = [.b,a.]
by A4, TOPMETR:18;
[.b,a.] c= the
carrier of
T
by A1, Th8;
then reconsider f =
L[01] (
((b,a) (#)),
((#) (b,a))) as
Function of
I[01],
T by A5, FUNCT_2:7, TOPMETR:20;
take
f
;
BORSUK_2:def 1 ( 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:7, TOPMETR:20;
L[01] (
((b,a) (#)),
((#) (b,a))) is
continuous
by A4, TREAL_1:8;
then
g is
continuous
by PRE_TOPC:26, TOPMETR:20;
hence
f is
continuous
by PRE_TOPC:27;
( f . 0 = a & f . 1 = b )thus f . 0 =
f . ((#) (0,1))
by TREAL_1:def 1
.=
(
b,
a)
(#)
by A4, TREAL_1:9
.=
a
by A4, TREAL_1:def 2
;
f . 1 = bthus f . 1 =
f . ((0,1) (#))
by TREAL_1:def 2
.=
(#) (
b,
a)
by A4, TREAL_1:9
.=
b
by A4, TREAL_1:def 1
;
verum end;