let n be Nat; for p1, p2 being Point of (TOP-REAL n)
for P being non empty Subset of (TOP-REAL n) st P is closed & P c= LSeg (p1,p2) holds
ex s being Real st
( ((1 - s) * p1) + (s * p2) in P & ( for r being Real st 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P holds
s <= r ) )
let p1, p2 be Point of (TOP-REAL n); for P being non empty Subset of (TOP-REAL n) st P is closed & P c= LSeg (p1,p2) holds
ex s being Real st
( ((1 - s) * p1) + (s * p2) in P & ( for r being Real st 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P holds
s <= r ) )
let P be non empty Subset of (TOP-REAL n); ( P is closed & P c= LSeg (p1,p2) implies ex s being Real st
( ((1 - s) * p1) + (s * p2) in P & ( for r being Real st 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P holds
s <= r ) ) )
set W = { r where r is Real : ( 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P ) } ;
{ r where r is Real : ( 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P ) } c= REAL
then reconsider W = { r where r is Real : ( 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P ) } as Subset of REAL ;
assume that
A1:
P is closed
and
A2:
P c= LSeg (p1,p2)
; ex s being Real st
( ((1 - s) * p1) + (s * p2) in P & ( for r being Real st 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P holds
s <= r ) )
take r2 = lower_bound W; ( ((1 - r2) * p1) + (r2 * p2) in P & ( for r being Real st 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P holds
r2 <= r ) )
A3:
W is bounded_below
hereby for r being Real st 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P holds
r2 <= r
set p =
((1 - r2) * p1) + (r2 * p2);
reconsider u =
((1 - r2) * p1) + (r2 * p2) as
Point of
(Euclid n) by EUCLID:22;
A4:
TopStruct(# the
carrier of
(TOP-REAL n), the
topology of
(TOP-REAL n) #)
= TopSpaceMetr (Euclid n)
by EUCLID:def 8;
then reconsider Q =
P ` as
Subset of
(TopSpaceMetr (Euclid n)) ;
P ` is
open
by A1, TOPS_1:3;
then A5:
Q is
open
by A4, PRE_TOPC:30;
A6:
ex
r0 being
Real st
r0 in W
assume A9:
not
((1 - r2) * p1) + (r2 * p2) in P
;
contradictionthen
((1 - r2) * p1) + (r2 * p2) in the
carrier of
(TOP-REAL n) \ P
by XBOOLE_0:def 5;
then consider r0 being
Real such that A10:
r0 > 0
and A11:
Ball (
u,
r0)
c= Q
by A5, TOPMETR:15;
per cases
( p1 <> p2 or p1 = p2 )
;
suppose A12:
p1 <> p2
;
contradictionreconsider v2 =
p2 as
Element of
REAL n by EUCLID:22;
reconsider v1 =
p1 as
Element of
REAL n by EUCLID:22;
A13:
|.(v2 - v1).| > 0
by A12, EUCLID:17;
then
r0 / |.(v2 - v1).| > 0
by A10, XREAL_1:139;
then consider r4 being
Real such that A14:
r4 in W
and A15:
r4 < r2 + (r0 / |.(v2 - v1).|)
by A3, A6, SEQ_4:def 2;
reconsider r4 =
r4 as
Real ;
r4 + 0 < r2 + (r0 / |.(v2 - v1).|)
by A15;
then A16:
r4 - r2 < (r0 / |.(v2 - v1).|) - 0
by XREAL_1:21;
set p3 =
((1 - r4) * p1) + (r4 * p2);
reconsider u3 =
((1 - r4) * p1) + (r4 * p2) as
Point of
(Euclid n) by EUCLID:22;
reconsider v3 =
((1 - r4) * p1) + (r4 * p2),
v4 =
((1 - r2) * p1) + (r2 * p2) as
Element of
REAL n by EUCLID:22;
A17:
(((1 - r4) * p1) + (r4 * p2)) - (((1 - r2) * p1) + (r2 * p2)) =
(((1 - r4) * p1) + (r4 * p2)) + ((- ((1 - r2) * p1)) - (r2 * p2))
by RLVECT_1:30
.=
((((1 - r4) * p1) + (r4 * p2)) + (- ((1 - r2) * p1))) + (- (r2 * p2))
by RLVECT_1:def 3
.=
((r4 * p2) + (((1 - r4) * p1) + (- ((1 - r2) * p1)))) + (- (r2 * p2))
by RLVECT_1:def 3
.=
((((1 - r4) * p1) + (- ((1 - r2) * p1))) + (r4 * p2)) + ((- r2) * p2)
by RLVECT_1:79
.=
((((1 - r4) * p1) + ((- (1 - r2)) * p1)) + (r4 * p2)) + ((- r2) * p2)
by RLVECT_1:79
.=
(((1 - r4) * p1) + ((- (1 - r2)) * p1)) + ((r4 * p2) + ((- r2) * p2))
by RLVECT_1:def 3
.=
(((1 - r4) * p1) + ((- (1 - r2)) * p1)) + ((r4 + (- r2)) * p2)
by RLVECT_1:def 6
.=
(((1 - r4) + (- (1 - r2))) * p1) + ((r4 - r2) * p2)
by RLVECT_1:def 6
.=
((- (r4 - r2)) * p1) + ((r4 - r2) * p2)
.=
((r4 - r2) * p2) - ((r4 - r2) * p1)
by RLVECT_1:79
.=
(r4 - r2) * (p2 - p1)
by RLVECT_1:34
.=
(r4 - r2) * (v2 - v1)
;
r2 <= r4
by A3, A14, SEQ_4:def 2;
then A18:
r4 - r2 >= 0
by XREAL_1:48;
dist (
u3,
u) =
|.(v3 - v4).|
by Th5
.=
|.((((1 - r4) * p1) + (r4 * p2)) - (((1 - r2) * p1) + (r2 * p2))).|
.=
|.((r4 - r2) * (v2 - v1)).|
by A17
.=
|.(r4 - r2).| * |.(v2 - v1).|
by EUCLID:11
.=
(r4 - r2) * |.(v2 - v1).|
by A18, ABSVALUE:def 1
;
then
dist (
u3,
u)
< (r0 / |.(v2 - v1).|) * |.(v2 - v1).|
by A13, A16, XREAL_1:68;
then
dist (
u,
u3)
< r0
by A13, XCMPLX_1:87;
then
u3 in { u0 where u0 is Point of (Euclid n) : dist (u,u0) < r0 }
;
then A19:
u3 in Ball (
u,
r0)
by METRIC_1:17;
ex
r being
Real st
(
r = r4 &
0 <= r &
r <= 1 &
((1 - r) * p1) + (r * p2) in P )
by A14;
hence
contradiction
by A11, A19, XBOOLE_0:def 5;
verum end; suppose A20:
p1 = p2
;
contradictionend; end;
end;
let r be Real; ( 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P implies r2 <= r )
assume
( 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P )
; r2 <= r
then
r in W
;
hence
r2 <= r
by A3, SEQ_4:def 2; verum