let n be Element of NAT ; for p1, p2 being Point of (TOP-REAL n) st p1 <> p2 holds
ex f being Function of I[01] ,((TOP-REAL n) | (LSeg p1,p2)) st
( ( for x being Real st x in [.0 ,1.] holds
f . x = ((1 - x) * p1) + (x * p2) ) & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 )
let p1, p2 be Point of (TOP-REAL n); ( p1 <> p2 implies ex f being Function of I[01] ,((TOP-REAL n) | (LSeg p1,p2)) st
( ( for x being Real st x in [.0 ,1.] holds
f . x = ((1 - x) * p1) + (x * p2) ) & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) )
reconsider p19 = p1, p29 = p2 as Element of REAL n by Lm1;
set P = LSeg p1,p2;
reconsider PP = LSeg p1,p2 as Subset of (Euclid n) by TOPREAL3:13;
reconsider PP = PP as non empty Subset of (Euclid n) ;
defpred S1[ set , set ] means for x being Real st x = $1 holds
$2 = ((1 - x) * p1) + (x * p2);
A1:
for a being set st a in [.0 ,1.] holds
ex u being set st S1[a,u]
proof
let a be
set ;
( a in [.0 ,1.] implies ex u being set st S1[a,u] )
assume
a in [.0 ,1.]
;
ex u being set st S1[a,u]
then reconsider x =
a as
Real ;
take
((1 - x) * p1) + (x * p2)
;
S1[a,((1 - x) * p1) + (x * p2)]
thus
S1[
a,
((1 - x) * p1) + (x * p2)]
;
verum
end;
consider f being Function such that
A2:
dom f = [.0 ,1.]
and
A3:
for a being set st a in [.0 ,1.] holds
S1[a,f . a]
from CLASSES1:sch 1(A1);
rng f c= the carrier of ((TOP-REAL n) | (LSeg p1,p2))
proof
let y be
set ;
TARSKI:def 3 ( not y in rng f or y in the carrier of ((TOP-REAL n) | (LSeg p1,p2)) )
assume
y in rng f
;
y in the carrier of ((TOP-REAL n) | (LSeg p1,p2))
then consider x being
set such that A4:
x in dom f
and A5:
y = f . x
by FUNCT_1:def 5;
x in { r where r is Real : ( 0 <= r & r <= 1 ) }
by A2, A4, RCOMP_1:def 1;
then consider r being
Real such that A6:
r = x
and A7:
(
0 <= r &
r <= 1 )
;
y = ((1 - r) * p1) + (r * p2)
by A2, A3, A4, A5, A6;
then
y in LSeg p1,
p2
by A7;
then
y in [#] ((TOP-REAL n) | (LSeg p1,p2))
by PRE_TOPC:def 10;
hence
y in the
carrier of
((TOP-REAL n) | (LSeg p1,p2))
;
verum
end;
then reconsider f = f as Function of I[01] ,((TOP-REAL n) | (LSeg p1,p2)) by A2, BORSUK_1:83, FUNCT_2:def 1, RELSET_1:11;
assume A8:
p1 <> p2
; ex f being Function of I[01] ,((TOP-REAL n) | (LSeg p1,p2)) st
( ( for x being Real st x in [.0 ,1.] holds
f . x = ((1 - x) * p1) + (x * p2) ) & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 )
now let x1,
x2 be
set ;
( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )assume that A9:
x1 in dom f
and A10:
x2 in dom f
and A11:
f . x1 = f . x2
;
x1 = x2
x2 in { r where r is Real : ( 0 <= r & r <= 1 ) }
by A2, A10, RCOMP_1:def 1;
then consider r2 being
Real such that A12:
r2 = x2
and
0 <= r2
and
r2 <= 1
;
A13:
f . x2 = ((1 - r2) * p1) + (r2 * p2)
by A2, A3, A10, A12;
x1 in { r where r is Real : ( 0 <= r & r <= 1 ) }
by A2, A9, RCOMP_1:def 1;
then consider r1 being
Real such that A14:
r1 = x1
and
0 <= r1
and
r1 <= 1
;
f . x1 = ((1 - r1) * p1) + (r1 * p2)
by A2, A3, A9, A14;
hence
x1 = x2
by A8, A11, A14, A12, A13, Th3;
verum end;
then A15:
f is one-to-one
by FUNCT_1:def 8;
A16:
(TOP-REAL n) | (LSeg p1,p2) = TopSpaceMetr ((Euclid n) | PP)
by EUCLID:67;
for W being Point of I[01]
for G being a_neighborhood of f . W ex H being a_neighborhood of W st f .: H c= G
proof
reconsider p11 =
p1,
p22 =
p2 as
Point of
(Euclid n) by TOPREAL3:13;
let W be
Point of
I[01] ;
for G being a_neighborhood of f . W ex H being a_neighborhood of W st f .: H c= Glet G be
a_neighborhood of
f . W;
ex H being a_neighborhood of W st f .: H c= G
reconsider W9 =
W as
Point of
(Closed-Interval-MSpace 0 ,1) by BORSUK_1:83, TOPMETR:14;
reconsider W1 =
W as
Real by BORSUK_1:83, TARSKI:def 3;
f . W in Int G
by CONNSP_2:def 1;
then consider Q being
Subset of
((TOP-REAL n) | (LSeg p1,p2)) such that A17:
Q is
open
and A18:
Q c= G
and A19:
f . W in Q
by TOPS_1:54;
[#] ((TOP-REAL n) | (LSeg p1,p2)) = LSeg p1,
p2
by PRE_TOPC:def 10;
then reconsider Y =
f . W as
Point of
((Euclid n) | PP) by TOPMETR:def 2;
consider r being
real number such that A20:
r > 0
and A21:
Ball Y,
r c= Q
by A16, A17, A19, TOPMETR:22;
reconsider r =
r as
Element of
REAL by XREAL_0:def 1;
set delta =
r / ((Pitag_dist n) . p19,p29);
reconsider H =
Ball W9,
(r / ((Pitag_dist n) . p19,p29)) as
Subset of
I[01] by BORSUK_1:83, TOPMETR:14;
Closed-Interval-TSpace 0 ,1
= TopSpaceMetr (Closed-Interval-MSpace 0 ,1)
by TOPMETR:def 8;
then A22:
H is
open
by TOPMETR:21, TOPMETR:27;
LSeg p1,
p2 = the
carrier of
((Euclid n) | PP)
by TOPMETR:def 2;
then reconsider WW9 =
Y as
Point of
(Euclid n) by TARSKI:def 3;
Euclid n = MetrStruct(#
(REAL n),
(Pitag_dist n) #)
by EUCLID:def 7;
then A23:
(Pitag_dist n) . p19,
p29 = dist p11,
p22
by METRIC_1:def 1;
A24:
(
dist p11,
p22 >= 0 &
dist p11,
p22 <> 0 )
by A8, METRIC_1:2, METRIC_1:5;
then
W in H
by A20, A23, TBSP_1:16, XREAL_1:141;
then
W in Int H
by A22, TOPS_1:55;
then reconsider H =
H as
a_neighborhood of
W by CONNSP_2:def 1;
take
H
;
f .: H c= G
A25:
r / ((Pitag_dist n) . p19,p29) > 0
by A20, A23, A24, XREAL_1:141;
f .: H c= Ball Y,
r
proof
reconsider WW1 =
WW9 as
Element of
REAL n by Lm1;
let a be
set ;
TARSKI:def 3 ( not a in f .: H or a in Ball Y,r )
A26:
[#] ((TOP-REAL n) | (LSeg p1,p2)) = LSeg p1,
p2
by PRE_TOPC:def 10;
assume
a in f .: H
;
a in Ball Y,r
then consider u being
set such that A27:
u in dom f
and A28:
u in H
and A29:
a = f . u
by FUNCT_1:def 12;
reconsider u1 =
u as
Real by A2, A27;
A30:
f . W = ((1 - W1) * p1) + (W1 * p2)
by A3, BORSUK_1:83;
reconsider u9 =
u as
Point of
(Closed-Interval-MSpace 0 ,1) by A28;
reconsider W99 =
W9,
u99 =
u9 as
Point of
RealSpace by TOPMETR:12;
A31:
dist W9,
u9 =
the
distance of
(Closed-Interval-MSpace 0 ,1) . W9,
u9
by METRIC_1:def 1
.=
the
distance of
RealSpace . W99,
u99
by TOPMETR:def 1
.=
dist W99,
u99
by METRIC_1:def 1
;
dist W9,
u9 < r / ((Pitag_dist n) . p19,p29)
by A28, METRIC_1:12;
then
abs (W1 - u1) < r / ((Pitag_dist n) . p19,p29)
by A31, TOPMETR:15;
then
abs (- (u1 - W1)) < r / ((Pitag_dist n) . p19,p29)
;
then A32:
abs (u1 - W1) < r / ((Pitag_dist n) . p19,p29)
by COMPLEX1:138;
A33:
r / ((Pitag_dist n) . p19,p29) <> 0
by A20, A23, A24, XREAL_1:141;
then
(Pitag_dist n) . p19,
p29 = r / (r / ((Pitag_dist n) . p19,p29))
by XCMPLX_1:54;
then A34:
|.(p19 - p29).| = r / (r / ((Pitag_dist n) . p19,p29))
by EUCLID:def 6;
f . u in rng f
by A27, FUNCT_1:def 5;
then reconsider aa =
a as
Point of
((Euclid n) | PP) by A29, A26, TOPMETR:def 2;
LSeg p1,
p2 = the
carrier of
((Euclid n) | PP)
by TOPMETR:def 2;
then reconsider aa9 =
aa as
Point of
(Euclid n) by TARSKI:def 3;
reconsider aa1 =
aa9 as
Element of
REAL n by Lm1;
A35:
p1 - p2 = p19 - p29
by EUCLID:73;
aa1 = ((1 - u1) * p1) + (u1 * p2)
by A2, A3, A27, A29;
then WW1 - aa1 =
(((1 - W1) * p1) + (W1 * p2)) - (((1 - u1) * p1) + (u1 * p2))
by A30, EUCLID:73
.=
(((W1 * p2) + ((1 - W1) * p1)) - ((1 - u1) * p1)) - (u1 * p2)
by EUCLID:50
.=
((W1 * p2) + (((1 - W1) * p1) - ((1 - u1) * p1))) - (u1 * p2)
by EUCLID:49
.=
((W1 * p2) + (((1 - W1) - (1 - u1)) * p1)) - (u1 * p2)
by EUCLID:54
.=
((u1 - W1) * p1) + ((W1 * p2) - (u1 * p2))
by EUCLID:49
.=
((u1 - W1) * p1) + ((W1 - u1) * p2)
by EUCLID:54
.=
((u1 - W1) * p1) + ((- (u1 - W1)) * p2)
.=
((u1 - W1) * p1) + (- ((u1 - W1) * p2))
by EUCLID:44
.=
((u1 - W1) * p1) - ((u1 - W1) * p2)
by EUCLID:45
.=
(u1 - W1) * (p1 - p2)
by EUCLID:53
.=
(u1 - W1) * (p19 - p29)
by A35, EUCLID:69
;
then A36:
|.(WW1 - aa1).| = (abs (u1 - W1)) * |.(p19 - p29).|
by EUCLID:14;
r / (r / ((Pitag_dist n) . p19,p29)) > 0
by A20, A25, XREAL_1:141;
then
|.(WW1 - aa1).| < (r / ((Pitag_dist n) . p19,p29)) * (r / (r / ((Pitag_dist n) . p19,p29)))
by A36, A32, A34, XREAL_1:70;
then
(
Euclid n = MetrStruct(#
(REAL n),
(Pitag_dist n) #) &
|.(WW1 - aa1).| < r )
by A33, EUCLID:def 7, XCMPLX_1:88;
then
the
distance of
(Euclid n) . WW9,
aa9 < r
by EUCLID:def 6;
then
the
distance of
((Euclid n) | PP) . Y,
aa < r
by TOPMETR:def 1;
then
dist Y,
aa < r
by METRIC_1:def 1;
hence
a in Ball Y,
r
by METRIC_1:12;
verum
end;
then
f .: H c= Q
by A21, XBOOLE_1:1;
hence
f .: H c= G
by A18, XBOOLE_1:1;
verum
end;
then A37:
f is continuous
by BORSUK_1:def 3;
take
f
; ( ( for x being Real st x in [.0 ,1.] holds
f . x = ((1 - x) * p1) + (x * p2) ) & f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 )
thus
for x being Real st x in [.0 ,1.] holds
f . x = ((1 - x) * p1) + (x * p2)
by A3; ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 )
[#] ((TOP-REAL n) | (LSeg p1,p2)) c= rng f
then
( [#] I[01] = [.0 ,1.] & rng f = [#] ((TOP-REAL n) | (LSeg p1,p2)) )
by BORSUK_1:83, XBOOLE_0:def 10;
hence
f is being_homeomorphism
by A2, A15, A37, COMPTS_1:26; ( f . 0 = p1 & f . 1 = p2 )
0 in [.0 ,1.]
by XXREAL_1:1;
hence f . 0 =
((1 - 0 ) * p1) + (0 * p2)
by A3
.=
p1 + (0 * p2)
by EUCLID:33
.=
p1 + (0. (TOP-REAL n))
by EUCLID:33
.=
p1
by EUCLID:31
;
f . 1 = p2
1 in [.0 ,1.]
by XXREAL_1:1;
hence f . 1 =
((1 - 1) * p1) + (1 * p2)
by A3
.=
(0. (TOP-REAL n)) + (1 * p2)
by EUCLID:33
.=
1 * p2
by EUCLID:31
.=
p2
by EUCLID:33
;
verum