let n be 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:8;
reconsider PP = PP as non empty Subset of (Euclid n) ;
defpred S1[ object , object ] means for x being Real st x = $1 holds
$2 = ((1 - x) * p1) + (x * p2);
A1:
for a being object st a in [.0,1.] holds
ex u being object st S1[a,u]
proof
let a be
object ;
( a in [.0,1.] implies ex u being object st S1[a,u] )
assume
a in [.0,1.]
;
ex u being object 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 object 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
object ;
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
object such that A4:
x in dom f
and A5:
y = f . x
by FUNCT_1:def 3;
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 5;
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:40, FUNCT_2:def 1, RELSET_1:4;
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 for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2let x1,
x2 be
object ;
( 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, Th2;
verum end;
then A15:
f is one-to-one
by FUNCT_1:def 4;
A16:
(TOP-REAL n) | (LSeg (p1,p2)) = TopSpaceMetr ((Euclid n) | PP)
by EUCLID:63;
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:8;
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:40, TOPMETR:10;
reconsider W1 =
W as
Real ;
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:22;
[#] ((TOP-REAL n) | (LSeg (p1,p2))) = LSeg (
p1,
p2)
by PRE_TOPC:def 5;
then reconsider Y =
f . W as
Point of
((Euclid n) | PP) by TOPMETR:def 2;
consider r being
Real such that A20:
r > 0
and A21:
Ball (
Y,
r)
c= Q
by A16, A17, A19, TOPMETR:15;
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:40, TOPMETR:10;
Closed-Interval-TSpace (
0,1)
= TopSpaceMetr (Closed-Interval-MSpace (0,1))
by TOPMETR:def 7;
then A22:
H is
open
by TOPMETR:14, TOPMETR:20;
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:11, XREAL_1:139;
then
W in Int H
by A22, TOPS_1:23;
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:139;
f .: H c= Ball (
Y,
r)
proof
reconsider WW1 =
WW9 as
Element of
REAL n by Lm1;
let a be
object ;
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 5;
assume
a in f .: H
;
a in Ball (Y,r)
then consider u being
object such that A27:
u in dom f
and A28:
u in H
and A29:
a = f . u
by FUNCT_1:def 6;
reconsider u1 =
u as
Real by A27;
A30:
f . W = ((1 - W1) * p1) + (W1 * p2)
by A3, BORSUK_1:40;
reconsider u9 =
u as
Point of
(Closed-Interval-MSpace (0,1)) by A28;
reconsider W99 =
W9,
u99 =
u9 as
Point of
RealSpace by TOPMETR:8;
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:11;
then
|.(W1 - u1).| < r / ((Pitag_dist n) . (p19,p29))
by A31, TOPMETR:11;
then
|.(- (u1 - W1)).| < r / ((Pitag_dist n) . (p19,p29))
;
then A32:
|.(u1 - W1).| < r / ((Pitag_dist n) . (p19,p29))
by COMPLEX1:52;
A33:
r / ((Pitag_dist n) . (p19,p29)) <> 0
by A20, A23, A24, XREAL_1:139;
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 3;
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;
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
.=
(((W1 * p2) + ((1 - W1) * p1)) - ((1 - u1) * p1)) - (u1 * p2)
by RLVECT_1:27
.=
((W1 * p2) + (((1 - W1) * p1) - ((1 - u1) * p1))) - (u1 * p2)
by RLVECT_1:def 3
.=
((W1 * p2) + (((1 - W1) - (1 - u1)) * p1)) - (u1 * p2)
by RLVECT_1:35
.=
((u1 - W1) * p1) + ((W1 * p2) - (u1 * p2))
by RLVECT_1:def 3
.=
((u1 - W1) * p1) + ((W1 - u1) * p2)
by RLVECT_1:35
.=
((u1 - W1) * p1) + ((- (u1 - W1)) * p2)
.=
((u1 - W1) * p1) + (- ((u1 - W1) * p2))
by RLVECT_1:79
.=
((u1 - W1) * p1) - ((u1 - W1) * p2)
.=
(u1 - W1) * (p1 - p2)
by RLVECT_1:34
.=
(u1 - W1) * (p19 - p29)
;
then A35:
|.(WW1 - aa1).| = |.(u1 - W1).| * |.(p19 - p29).|
by EUCLID:11;
r / (r / ((Pitag_dist n) . (p19,p29))) > 0
by A20, A25, XREAL_1:139;
then
|.(WW1 - aa1).| < (r / ((Pitag_dist n) . (p19,p29))) * (r / (r / ((Pitag_dist n) . (p19,p29))))
by A35, A32, A34, XREAL_1:68;
then
(
Euclid n = MetrStruct(#
(REAL n),
(Pitag_dist n) #) &
|.(WW1 - aa1).| < r )
by A33, EUCLID:def 7, XCMPLX_1:87;
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:11;
verum
end;
then
f .: H c= Q
by A21;
hence
f .: H c= G
by A18;
verum
end;
then A36:
f is continuous
by BORSUK_1:def 1;
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:40;
hence
f is being_homeomorphism
by A15, A36, COMPTS_1:17; ( 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 RLVECT_1:def 8
.=
p1 + (0. (TOP-REAL n))
by RLVECT_1:10
.=
p1
by RLVECT_1:4
;
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 RLVECT_1:10
.=
1 * p2
by RLVECT_1:4
.=
p2
by RLVECT_1:def 8
;
verum