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:67;
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:22;
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);
A4:
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 A5:
x in dom f
and A6:
y = f . x
by FUNCT_1:def 3;
x in { r where r is Real : ( 0 <= r & r <= 1 ) }
by A2, A5, RCOMP_1:def 1;
then consider r being
Real such that A7:
r = x
and A8:
0 <= r
and A9:
r <= 1
;
y = ((1 - r) * p1) + (r * p2)
by A2, A3, A5, A6, A7;
then
y in { (((1 - lambda) * p1) + (lambda * p2)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) }
by A8, A9;
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;
A10:
I[01] is compact
by HEINE:4, TOPMETR:20;
assume A11:
p1 <> p2
; LSeg (p1,p2) is_an_arc_of p1,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 A12:
x1 in dom f
and A13:
x2 in dom f
and A14:
f . x1 = f . x2
;
x1 = x2
x2 in { r where r is Real : ( 0 <= r & r <= 1 ) }
by A2, A13, RCOMP_1:def 1;
then consider r2 being
Real such that A15:
r2 = x2
and
0 <= r2
and
r2 <= 1
;
A16:
f . x2 = ((1 - r2) * p1) + (r2 * p2)
by A2, A3, A13, A15;
x1 in { r where r is Real : ( 0 <= r & r <= 1 ) }
by A2, A12, RCOMP_1:def 1;
then consider r1 being
Real such that A17:
r1 = x1
and
0 <= r1
and
r1 <= 1
;
f . x1 = ((1 - r1) * p1) + (r1 * p2)
by A2, A3, A12, A17;
then
(((1 - r1) * p1) + (r1 * p2)) + ((- r1) * p2) = ((1 - r2) * p1) + ((r2 * p2) + ((- r1) * p2))
by A14, A16, RLVECT_1:def 3;
then
(((1 - r1) * p1) + (r1 * p2)) + ((- r1) * p2) = ((1 - r2) * p1) + ((r2 + (- r1)) * p2)
by RLVECT_1:def 6;
then
((1 - r1) * p1) + ((r1 * p2) + ((- r1) * p2)) = ((1 - r2) * p1) + ((r2 - r1) * p2)
by RLVECT_1:def 3;
then
((1 - r1) * p1) + ((r1 + (- r1)) * p2) = ((1 - r2) * p1) + ((r2 - r1) * p2)
by RLVECT_1:def 6;
then
((1 - r1) * p1) + (0. (TOP-REAL n)) = ((1 - r2) * p1) + ((r2 - r1) * p2)
by RLVECT_1:10;
then
((- (1 - r2)) * p1) + ((1 - r1) * p1) = ((- (1 - r2)) * p1) + (((1 - r2) * p1) + ((r2 - r1) * p2))
by RLVECT_1:4;
then
((- (1 - r2)) * p1) + ((1 - r1) * p1) = (((- (1 - r2)) * p1) + ((1 - r2) * p1)) + ((r2 - r1) * p2)
by RLVECT_1:def 3;
then
((- (1 - r2)) * p1) + ((1 - r1) * p1) = (((- (1 - r2)) + (1 - r2)) * p1) + ((r2 - r1) * p2)
by RLVECT_1:def 6;
then
((- (1 - r2)) * p1) + ((1 - r1) * p1) = (0. (TOP-REAL n)) + ((r2 - r1) * p2)
by RLVECT_1:10;
then
((- (1 - r2)) * p1) + ((1 - r1) * p1) = (r2 - r1) * p2
by RLVECT_1:4;
then
((r2 - 1) + (1 - r1)) * p1 = (r2 - r1) * p2
by RLVECT_1:def 6;
then
r2 - r1 = 0
by A11, RLVECT_1:36;
hence
x1 = x2
by A17, A15;
verum end;
then A18:
f is one-to-one
;
[#] ((TOP-REAL n) | (LSeg (p1,p2))) c= rng f
then A23:
rng f = [#] ((TOP-REAL n) | (LSeg (p1,p2)))
by A4;
A24:
TopSpaceMetr (Euclid n) is T_2
by PCOMPS_1:34;
A25:
(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 EUCLID:67;
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;
A26:
(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 5;
then reconsider Y =
f . W as
Point of
((Euclid n) | PP) by TOPMETR:def 2;
A27:
dist (
p11,
p22)
>= 0
by METRIC_1:5;
reconsider W1 =
W as
Real ;
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 A28:
Q is
open
and A29:
Q c= G
and A30:
f . W in Q
by TOPS_1:22;
consider r being
Real such that A31:
r > 0
and A32:
Ball (
Y,
r)
c= Q
by A25, A28, A30, 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 A33:
H is
open
by TOPMETR:14, TOPMETR:20;
A34:
dist (
p11,
p22)
<> 0
by A11, METRIC_1:2;
then
W in H
by A31, A26, A27, TBSP_1:11, XREAL_1:139;
then
W in Int H
by A33, TOPS_1:23;
then reconsider H =
H as
a_neighborhood of
W by CONNSP_2:def 1;
take
H
;
f .: H c= G
A35:
r / ((Pitag_dist n) . (p19,p29)) > 0
by A31, A26, A27, A34, XREAL_1:139;
f .: H c= Ball (
Y,
r)
proof
reconsider WW1 =
WW9 as
Element of
REAL n ;
let a be
object ;
TARSKI:def 3 ( not a in f .: H or a in Ball (Y,r) )
A36:
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
object such that A37:
u in dom f
and A38:
u in H
and A39:
a = f . u
by FUNCT_1:def 6;
reconsider u1 =
u as
Real by A2, A37;
A40:
[#] ((TOP-REAL n) | (LSeg (p1,p2))) = LSeg (
p1,
p2)
by PRE_TOPC:def 5;
reconsider u9 =
u as
Point of
(Closed-Interval-MSpace (0,1)) by A38;
reconsider W99 =
W9,
u99 =
u9 as
Point of
RealSpace by TOPMETR:8;
A41:
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 A38, METRIC_1:11;
then
|.(W1 - u1).| < r / ((Pitag_dist n) . (p19,p29))
by A41, TOPMETR:11;
then
|.(- (u1 - W1)).| < r / ((Pitag_dist n) . (p19,p29))
;
then A42:
|.(u1 - W1).| < r / ((Pitag_dist n) . (p19,p29))
by COMPLEX1:52;
A43:
r / ((Pitag_dist n) . (p19,p29)) <> 0
by A31, A26, A27, A34, XREAL_1:139;
then
(Pitag_dist n) . (
p19,
p29)
= r / (r / ((Pitag_dist n) . (p19,p29)))
by XCMPLX_1:54;
then A44:
|.(p19 - p29).| = r / (r / ((Pitag_dist n) . (p19,p29)))
by EUCLID:def 6;
f . u in rng f
by A37, FUNCT_1:def 3;
then reconsider aa =
a as
Point of
((Euclid n) | PP) by A39, A36, A40, 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 ;
A45:
p19 - p29 = p1 - p2
by EUCLID:69;
A46:
WW1 = ((1 - W1) * p1) + (W1 * p2)
by A3, BORSUK_1:40;
aa1 = ((1 - u1) * p1) + (u1 * p2)
by A2, A3, A37, A39;
then WW1 - aa1 =
(((1 - W1) * p1) + (W1 * p2)) - (((1 - u1) * p1) + (u1 * p2))
by A46, EUCLID:69
.=
(((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)
by A45, EUCLID:65
;
then A47:
|.(WW1 - aa1).| = |.(u1 - W1).| * |.(p19 - p29).|
by EUCLID:11;
r / (r / ((Pitag_dist n) . (p19,p29))) > 0
by A31, A35, XREAL_1:139;
then
|.(WW1 - aa1).| < (r / ((Pitag_dist n) . (p19,p29))) * (r / (r / ((Pitag_dist n) . (p19,p29))))
by A47, A42, A44, XREAL_1:68;
then
|.(WW1 - aa1).| < r
by A43, 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 A32;
hence
f .: H c= G
by A29;
verum
end;
then A48:
f is continuous
by BORSUK_1:def 1;
take
f
; TOPREAL1:def 1 ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 )
A49:
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 A49, PRE_TOPC:36;
then
(TOP-REAL n) | (LSeg (p1,p2)) is T_2
by A24, TOPMETR:2;
hence
f is being_homeomorphism
by A23, A18, A48, A10, 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