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