let n be Nat; for p1, p2 being Point of (TOP-REAL n) st p1 <> p2 holds
LSeg p1,p2 is_an_arc_of p1,p2
let p1, p2 be Point of (TOP-REAL n); ( p1 <> p2 implies LSeg p1,p2 is_an_arc_of p1,p2 )
set P = LSeg p1,p2;
reconsider PP = LSeg p1,p2 as Subset of (Euclid n) by EUCLID:71;
not PP is empty
;
then reconsider PP = LSeg p1,p2 as non empty Subset of (Euclid n) ;
reconsider p19 = p1, p29 = p2 as Element of REAL n by EUCLID:25;
defpred S1[ set , set ] means for x being Real st x = $1 holds
$2 = ((1 - x) * p1) + (x * p2);
A1:
[#] I[01] = [.0 ,1.]
by BORSUK_1:83;
A2:
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
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);
A5:
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 A6:
x in dom f
and A7:
y = f . x
by FUNCT_1:def 5;
x in { r where r is Real : ( 0 <= r & r <= 1 ) }
by A3, A6, RCOMP_1:def 1;
then consider r being
Real such that A8:
r = x
and A9:
0 <= r
and A10:
r <= 1
;
y = ((1 - r) * p1) + (r * p2)
by A3, A4, A6, A7, A8;
then
y in { (((1 - lambda) * p1) + (lambda * p2)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) }
by A9, A10;
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 A3, BORSUK_1:83, FUNCT_2:def 1, RELSET_1:11;
A11:
I[01] is compact
by HEINE:11, TOPMETR:27;
assume A12:
p1 <> p2
; LSeg p1,p2 is_an_arc_of p1,p2
now let x1,
x2 be
set ;
( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )assume that A13:
x1 in dom f
and A14:
x2 in dom f
and A15:
f . x1 = f . x2
;
x1 = x2
x2 in { r where r is Real : ( 0 <= r & r <= 1 ) }
by A3, A14, RCOMP_1:def 1;
then consider r2 being
Real such that A16:
r2 = x2
and
0 <= r2
and
r2 <= 1
;
A17:
f . x2 = ((1 - r2) * p1) + (r2 * p2)
by A3, A4, A14, A16;
x1 in { r where r is Real : ( 0 <= r & r <= 1 ) }
by A3, A13, RCOMP_1:def 1;
then consider r1 being
Real such that A18:
r1 = x1
and
0 <= r1
and
r1 <= 1
;
f . x1 = ((1 - r1) * p1) + (r1 * p2)
by A3, A4, A13, A18;
then
(((1 - r1) * p1) + (r1 * p2)) + ((- r1) * p2) = ((1 - r2) * p1) + ((r2 * p2) + ((- r1) * p2))
by A15, A17, EUCLID:30;
then
(((1 - r1) * p1) + (r1 * p2)) + ((- r1) * p2) = ((1 - r2) * p1) + ((r2 + (- r1)) * p2)
by EUCLID:37;
then
((1 - r1) * p1) + ((r1 * p2) + ((- r1) * p2)) = ((1 - r2) * p1) + ((r2 - r1) * p2)
by EUCLID:30;
then
((1 - r1) * p1) + ((r1 + (- r1)) * p2) = ((1 - r2) * p1) + ((r2 - r1) * p2)
by EUCLID:37;
then
((1 - r1) * p1) + (0. (TOP-REAL n)) = ((1 - r2) * p1) + ((r2 - r1) * p2)
by EUCLID:33;
then
((- (1 - r2)) * p1) + ((1 - r1) * p1) = ((- (1 - r2)) * p1) + (((1 - r2) * p1) + ((r2 - r1) * p2))
by EUCLID:31;
then
((- (1 - r2)) * p1) + ((1 - r1) * p1) = (((- (1 - r2)) * p1) + ((1 - r2) * p1)) + ((r2 - r1) * p2)
by EUCLID:30;
then
((- (1 - r2)) * p1) + ((1 - r1) * p1) = (((- (1 - r2)) + (1 - r2)) * p1) + ((r2 - r1) * p2)
by EUCLID:37;
then
((- (1 - r2)) * p1) + ((1 - r1) * p1) = (0. (TOP-REAL n)) + ((r2 - r1) * p2)
by EUCLID:33;
then
((- (1 - r2)) * p1) + ((1 - r1) * p1) = (r2 - r1) * p2
by EUCLID:31;
then
((r2 - 1) + (1 - r1)) * p1 = (r2 - r1) * p2
by EUCLID:37;
then
r2 - r1 = 0
by A12, EUCLID:38;
hence
x1 = x2
by A18, A16;
verum end;
then A19:
f is one-to-one
by FUNCT_1:def 8;
[#] ((TOP-REAL n) | (LSeg p1,p2)) c= rng f
then A24:
rng f = [#] ((TOP-REAL n) | (LSeg p1,p2))
by A5, XBOOLE_0:def 10;
A25:
TopSpaceMetr (Euclid n) is T_2
by PCOMPS_1:38;
A26:
(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 EUCLID:71;
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;
A27:
(Pitag_dist n) . p19,
p29 = dist p11,
p22
by METRIC_1:def 1;
[#] ((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;
A28:
dist p11,
p22 >= 0
by METRIC_1:5;
reconsider W1 =
W as
Real by BORSUK_1:83, TARSKI:def 3;
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;
f . W in Int G
by CONNSP_2:def 1;
then consider Q being
Subset of
((TOP-REAL n) | (LSeg p1,p2)) such that A29:
Q is
open
and A30:
Q c= G
and A31:
f . W in Q
by TOPS_1:54;
consider r being
real number such that A32:
r > 0
and A33:
Ball Y,
r c= Q
by A26, A29, A31, 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 A34:
H is
open
by TOPMETR:21, TOPMETR:27;
A35:
dist p11,
p22 <> 0
by A12, METRIC_1:2;
then
W in H
by A32, A27, A28, TBSP_1:16, XREAL_1:141;
then
W in Int H
by A34, TOPS_1:55;
then reconsider H =
H as
a_neighborhood of
W by CONNSP_2:def 1;
take
H
;
f .: H c= G
A36:
r / ((Pitag_dist n) . p19,p29) > 0
by A32, A27, A28, A35, XREAL_1:141;
f .: H c= Ball Y,
r
proof
reconsider WW1 =
WW9 as
Element of
REAL n ;
let a be
set ;
TARSKI:def 3 ( not a in f .: H or a in Ball Y,r )
A37:
rng f c= the
carrier of
((TOP-REAL n) | (LSeg p1,p2))
by RELAT_1:def 19;
assume
a in f .: H
;
a in Ball Y,r
then consider u being
set such that A38:
u in dom f
and A39:
u in H
and A40:
a = f . u
by FUNCT_1:def 12;
reconsider u1 =
u as
Real by A3, A38;
A41:
[#] ((TOP-REAL n) | (LSeg p1,p2)) = LSeg p1,
p2
by PRE_TOPC:def 10;
reconsider u9 =
u as
Point of
(Closed-Interval-MSpace 0 ,1) by A39;
reconsider W99 =
W9,
u99 =
u9 as
Point of
RealSpace by TOPMETR:12;
A42:
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 A39, METRIC_1:12;
then
abs (W1 - u1) < r / ((Pitag_dist n) . p19,p29)
by A42, TOPMETR:15;
then
abs (- (u1 - W1)) < r / ((Pitag_dist n) . p19,p29)
;
then A43:
abs (u1 - W1) < r / ((Pitag_dist n) . p19,p29)
by COMPLEX1:138;
A44:
r / ((Pitag_dist n) . p19,p29) <> 0
by A32, A27, A28, A35, XREAL_1:141;
then
(Pitag_dist n) . p19,
p29 = r / (r / ((Pitag_dist n) . p19,p29))
by XCMPLX_1:54;
then A45:
|.(p19 - p29).| = r / (r / ((Pitag_dist n) . p19,p29))
by EUCLID:def 6;
f . u in rng f
by A38, FUNCT_1:def 5;
then reconsider aa =
a as
Point of
((Euclid n) | PP) by A40, A37, A41, 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 ;
A46:
p19 - p29 = p1 - p2
by EUCLID:73;
A47:
WW1 = ((1 - W1) * p1) + (W1 * p2)
by A4, BORSUK_1:83;
aa1 = ((1 - u1) * p1) + (u1 * p2)
by A3, A4, A38, A40;
then WW1 - aa1 =
(((1 - W1) * p1) + (W1 * p2)) - (((1 - u1) * p1) + (u1 * p2))
by A47, 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 A46, EUCLID:69
;
then A48:
|.(WW1 - aa1).| = (abs (u1 - W1)) * |.(p19 - p29).|
by EUCLID:14;
r / (r / ((Pitag_dist n) . p19,p29)) > 0
by A32, A36, XREAL_1:141;
then
|.(WW1 - aa1).| < (r / ((Pitag_dist n) . p19,p29)) * (r / (r / ((Pitag_dist n) . p19,p29)))
by A48, A43, A45, XREAL_1:70;
then
|.(WW1 - aa1).| < r
by A44, 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 A33, XBOOLE_1:1;
hence
f .: H c= G
by A30, XBOOLE_1:1;
verum
end;
then A49:
f is continuous
by BORSUK_1:def 3;
take
f
; TOPREAL1:def 2 ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 )
A50:
TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n)
by EUCLID:def 8;
then reconsider PP = LSeg p1,p2 as Subset of (TopSpaceMetr (Euclid n)) ;
(TopSpaceMetr (Euclid n)) | PP = (TOP-REAL n) | (LSeg p1,p2)
by A50, PRE_TOPC:66;
then
(TOP-REAL n) | (LSeg p1,p2) is T_2
by A25, TOPMETR:3;
hence
f is being_homeomorphism
by A3, A1, A24, A19, A49, A11, 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 A4
.=
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 A4
.=
(0. (TOP-REAL n)) + (1 * p2)
by EUCLID:33
.=
1 * p2
by EUCLID:31
.=
p2
by EUCLID:33
;
verum