let n be Nat; :: thesis: for p, q being Point of (TOP-REAL n)
for A being Subset of (TOP-REAL n) st p in A & p <> q & A /\ (halfline (p,q)) is bounded holds
ex w being Point of (Euclid n) st
( w in (Fr A) /\ (halfline (p,q)) & ( for u, P being Point of (Euclid n) st P = p & u in A /\ (halfline (p,q)) holds
dist (P,u) <= dist (P,w) ) & ( for r being Real st r > 0 holds
ex u being Point of (Euclid n) st
( u in A /\ (halfline (p,q)) & dist (w,u) < r ) ) )
let p, q be Point of (TOP-REAL n); :: thesis: for A being Subset of (TOP-REAL n) st p in A & p <> q & A /\ (halfline (p,q)) is bounded holds
ex w being Point of (Euclid n) st
( w in (Fr A) /\ (halfline (p,q)) & ( for u, P being Point of (Euclid n) st P = p & u in A /\ (halfline (p,q)) holds
dist (P,u) <= dist (P,w) ) & ( for r being Real st r > 0 holds
ex u being Point of (Euclid n) st
( u in A /\ (halfline (p,q)) & dist (w,u) < r ) ) )
set TRn = TOP-REAL n;
let A be Subset of (TOP-REAL n); :: thesis: ( p in A & p <> q & A /\ (halfline (p,q)) is bounded implies ex w being Point of (Euclid n) st
( w in (Fr A) /\ (halfline (p,q)) & ( for u, P being Point of (Euclid n) st P = p & u in A /\ (halfline (p,q)) holds
dist (P,u) <= dist (P,w) ) & ( for r being Real st r > 0 holds
ex u being Point of (Euclid n) st
( u in A /\ (halfline (p,q)) & dist (w,u) < r ) ) ) )
assume that
A1: p in A and
A2: p <> q and
A3: A /\ (halfline (p,q)) is bounded ; :: thesis: ex w being Point of (Euclid n) st
( w in (Fr A) /\ (halfline (p,q)) & ( for u, P being Point of (Euclid n) st P = p & u in A /\ (halfline (p,q)) holds
dist (P,u) <= dist (P,w) ) & ( for r being Real st r > 0 holds
ex u being Point of (Euclid n) st
( u in A /\ (halfline (p,q)) & dist (w,u) < r ) ) )
reconsider P = p, Q = q as Element of (Euclid n) by EUCLID:67;
A4: dist (P,Q) > 0 by A2, METRIC_1:7;
set H = halfline (p,q);
reconsider AH = A /\ (halfline (p,q)) as bounded Subset of (Euclid n) by A3, JORDAN2C:11;
A5: dist (Q,P) = |.(q - p).| by SPPOL_1:39;
p in halfline (p,q) by TOPREAL9:27;
then A6: p in AH by A1, XBOOLE_0:def 4;
set DAH = diameter AH;
set X = { r where r is Real : ( ((1 - r) * p) + (r * q) in AH & 0 <= r ) } ;
set dAH = (diameter AH) + 1;
A7: now :: thesis: for x being object st x in { r where r is Real : ( ((1 - r) * p) + (r * q) in AH & 0 <= r ) } holds
x is real
let x be object ; :: thesis: ( x in { r where r is Real : ( ((1 - r) * p) + (r * q) in AH & 0 <= r ) } implies x is real )
assume x in { r where r is Real : ( ((1 - r) * p) + (r * q) in AH & 0 <= r ) } ; :: thesis: x is real
then ex r being Real st
( x = r & ((1 - r) * p) + (r * q) in AH & 0 <= r ) ;
hence x is real ; :: thesis: verum
end;
( 1 * p = p & 0 * q = 0. (TOP-REAL n) ) by RLVECT_1:10, RLVECT_1:def 8;
then p = ((1 - 0) * p) + (0 * q) ;
then A8: 0 in { r where r is Real : ( ((1 - r) * p) + (r * q) in AH & 0 <= r ) } by A6;
then reconsider X = { r where r is Real : ( ((1 - r) * p) + (r * q) in AH & 0 <= r ) } as non empty real-membered set by A7, MEMBERED:def 3;
A9: (diameter AH) + 0 < (diameter AH) + 1 by XREAL_1:8;
now :: thesis: for x being ExtReal st x in X holds
x <= ((diameter AH) + 1) / (dist (Q,P))
let x be ExtReal; :: thesis: ( x in X implies x <= ((diameter AH) + 1) / (dist (Q,P)) )
assume x in X ; :: thesis: x <= ((diameter AH) + 1) / (dist (Q,P))
then consider r being Real such that
A10: x = r and
A11: ((1 - r) * p) + (r * q) in AH and
A12: 0 <= r ;
reconsider PQ = ((1 - r) * p) + (r * q) as Element of (Euclid n) by A11;
(((1 - r) * p) + (r * q)) - p = r * (q - p) by Lm1;
then dist (PQ,P) = |.(r * (q - p)).| by SPPOL_1:39
.= |.r.| * |.(q - p).| by TOPRNS_1:7
.= r * (dist (Q,P)) by A5, A12, ABSVALUE:def 1 ;
then r * (dist (Q,P)) <= diameter AH by A6, A11, TBSP_1:def 8;
then A13: r * (dist (Q,P)) <= (diameter AH) + 1 by A9, XXREAL_0:2;
(r * (dist (Q,P))) / (dist (Q,P)) = r * ((dist (Q,P)) / (dist (Q,P)))
.= r * 1 by A4, XCMPLX_1:60 ;
hence x <= ((diameter AH) + 1) / (dist (Q,P)) by A10, A13, XREAL_1:72; :: thesis: verum
end;
then ((diameter AH) + 1) / (dist (P,Q)) is UpperBound of X by XXREAL_2:def 1;
then X is bounded_above by XXREAL_2:def 10;
then reconsider S = sup X as Element of REAL by XXREAL_2:16;
A14: 0 <= S by A8, XXREAL_2:4;
set Spq = ((1 - S) * p) + (S * q);
reconsider spq = ((1 - S) * p) + (S * q) as Element of (Euclid n) by EUCLID:67;
A15: for r being Real st r > 0 holds
ex w being Point of (Euclid n) st
( w in AH & dist (spq,w) < r )
proof
let r be Real; :: thesis: ( r > 0 implies ex w being Point of (Euclid n) st
( w in AH & dist (spq,w) < r ) )
assume A16: r > 0 ; :: thesis: ex w being Point of (Euclid n) st
( w in AH & dist (spq,w) < r )
set r2 = r / |.(q - p).|;
assume A17: for w being Point of (Euclid n) st w in AH holds
dist (spq,w) >= r ; :: thesis: contradiction
now :: thesis: for x being ExtReal st x in X holds
S - (r / |.(q - p).|) >= x
let x be ExtReal; :: thesis: ( x in X implies S - (r / |.(q - p).|) >= x )
assume A18: x in X ; :: thesis: S - (r / |.(q - p).|) >= x
then consider w being Real such that
A19: x = w and
A20: ((1 - w) * p) + (w * q) in AH and
0 <= w ;
S - w >= 0 by A18, A19, XREAL_1:48, XXREAL_2:4;
then A21: |.(S - w).| = S - w by ABSVALUE:def 1;
reconsider PQ = ((1 - w) * p) + (w * q) as Element of (Euclid n) by A20;
A22: PQ = p + (w * (q - p)) by Th1;
(((1 - S) * p) + (S * q)) - (p + (w * (q - p))) = ((((1 - S) * p) + (S * q)) - p) - (w * (q - p)) by RLVECT_1:27
.= (S * (q - p)) - (w * (q - p)) by Lm1
.= (S - w) * (q - p) by RLVECT_1:35 ;
then dist (spq,PQ) = |.((S - w) * (q - p)).| by A22, SPPOL_1:39
.= (S - w) * |.(q - p).| by A21, TOPRNS_1:7 ;
then (S - w) * |.(q - p).| >= r by A17, A20;
then S - w >= r / |.(q - p).| by A2, A5, METRIC_1:7, XREAL_1:79;
hence S - (r / |.(q - p).|) >= x by A19, XREAL_1:11; :: thesis: verum
end;
then S - (r / |.(q - p).|) is UpperBound of X by XXREAL_2:def 1;
then S - 0 <= S - (r / |.(q - p).|) by XXREAL_2:def 3;
hence contradiction by A4, A5, A16, XREAL_1:8; :: thesis: verum
end;
A23: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
now :: thesis: for U being Subset of (TOP-REAL n) st U is open & ((1 - S) * p) + (S * q) in U holds
( A meets U & U \ A <> {} )
let U be Subset of (TOP-REAL n); :: thesis: ( U is open & ((1 - S) * p) + (S * q) in U implies ( A meets U & U \ A <> {} ) )
reconsider UE = U as Subset of (TopSpaceMetr (Euclid n)) by A23;
assume that
A24: U is open and
A25: ((1 - S) * p) + (S * q) in U ; :: thesis: ( A meets U & U \ A <> {} )
UE in the topology of (TopSpaceMetr (Euclid n)) by A23, A24, PRE_TOPC:def 2;
then UE is open by PRE_TOPC:def 2;
then consider r being Real such that
A26: r > 0 and
A27: Ball (spq,r) c= UE by A25, TOPMETR:15;
set r2 = r / |.(q - p).|;
set Sr = S + ((r / |.(q - p).|) / 2);
consider w being Element of (Euclid n) such that
A28: ( w in AH & dist (spq,w) < r ) by A15, A26;
( w in Ball (spq,r) & w in A ) by A28, METRIC_1:11, XBOOLE_0:def 4;
hence A meets U by A27, XBOOLE_0:3; :: thesis: U \ A <> {}
A29: (r / |.(q - p).|) * |.(q - p).| = r * (|.(q - p).| / |.(q - p).|)
.= r * 1 by A4, A5, XCMPLX_1:60 ;
S + ((r / |.(q - p).|) / 2) > S + 0 by A4, A5, A26, XREAL_1:6;
then S - (S + ((r / |.(q - p).|) / 2)) < 0 by XREAL_1:49;
then A30: |.(S - (S + ((r / |.(q - p).|) / 2))).| = - (S - (S + ((r / |.(q - p).|) / 2))) by ABSVALUE:def 1
.= (r / |.(q - p).|) / 2 ;
set Srpq = ((1 - (S + ((r / |.(q - p).|) / 2))) * p) + ((S + ((r / |.(q - p).|) / 2)) * q);
reconsider srpq = ((1 - (S + ((r / |.(q - p).|) / 2))) * p) + ((S + ((r / |.(q - p).|) / 2)) * q) as Element of (Euclid n) by EUCLID:67;
A31: srpq in halfline (p,q) by A14, A26;
A32: not srpq in A
proof
assume srpq in A ; :: thesis: contradiction
then srpq in AH by A31, XBOOLE_0:def 4;
then S + ((r / |.(q - p).|) / 2) in X by A14, A26;
then S + ((r / |.(q - p).|) / 2) <= S + 0 by XXREAL_2:4;
hence contradiction by A4, A5, A26, XREAL_1:8; :: thesis: verum
end;
(((1 - S) * p) + (S * q)) - (((1 - (S + ((r / |.(q - p).|) / 2))) * p) + ((S + ((r / |.(q - p).|) / 2)) * q)) = (((1 - S) * p) + (S * q)) - (p + ((S + ((r / |.(q - p).|) / 2)) * (q - p))) by Th1
.= ((((1 - S) * p) + (S * q)) - p) - ((S + ((r / |.(q - p).|) / 2)) * (q - p)) by RLVECT_1:27
.= (S * (q - p)) - ((S + ((r / |.(q - p).|) / 2)) * (q - p)) by Lm1
.= (S - (S + ((r / |.(q - p).|) / 2))) * (q - p) by RLVECT_1:35 ;
then dist (spq,srpq) = |.((S - (S + ((r / |.(q - p).|) / 2))) * (q - p)).| by SPPOL_1:39
.= ((r / |.(q - p).|) / 2) * |.(q - p).| by A30, TOPRNS_1:7
.= r / 2 by A29 ;
then dist (spq,srpq) < r by A26, XREAL_1:216;
then srpq in Ball (spq,r) by METRIC_1:11;
hence U \ A <> {} by A27, A32, XBOOLE_0:def 5; :: thesis: verum
end;
then A33: ((1 - S) * p) + (S * q) in Fr A by TOPGEN_1:9;
take spq ; :: thesis: ( spq in (Fr A) /\ (halfline (p,q)) & ( for u, P being Point of (Euclid n) st P = p & u in A /\ (halfline (p,q)) holds
dist (P,u) <= dist (P,spq) ) & ( for r being Real st r > 0 holds
ex u being Point of (Euclid n) st
( u in A /\ (halfline (p,q)) & dist (spq,u) < r ) ) )
A34: (((1 - S) * p) + (S * q)) - p = S * (q - p) by Lm1;
((1 - S) * p) + (S * q) in halfline (p,q) by A14;
hence spq in (Fr A) /\ (halfline (p,q)) by A33, XBOOLE_0:def 4; :: thesis: ( ( for u, P being Point of (Euclid n) st P = p & u in A /\ (halfline (p,q)) holds
dist (P,u) <= dist (P,spq) ) & ( for r being Real st r > 0 holds
ex u being Point of (Euclid n) st
( u in A /\ (halfline (p,q)) & dist (spq,u) < r ) ) )
A35: |.S.| = S by A14, ABSVALUE:def 1;
hereby :: thesis: for r being Real st r > 0 holds
ex u being Point of (Euclid n) st
( u in A /\ (halfline (p,q)) & dist (spq,u) < r )
let u, P be Point of (Euclid n); :: thesis: ( P = p & u in A /\ (halfline (p,q)) implies dist (P,u) <= dist (P,spq) )
assume that
A36: P = p and
A37: u in A /\ (halfline (p,q)) ; :: thesis: dist (P,u) <= dist (P,spq)
A38: dist (P,spq) = |.(S * (q - p)).| by A34, A36, SPPOL_1:39
.= S * |.(q - p).| by A35, TOPRNS_1:7 ;
u in halfline (p,q) by A37, XBOOLE_0:def 4;
then consider Ur being Real such that
A39: u = ((1 - Ur) * p) + (Ur * q) and
A40: 0 <= Ur ;
A41: |.Ur.| = Ur by A40, ABSVALUE:def 1;
Ur in X by A37, A39, A40;
then A42: Ur <= S by XXREAL_2:4;
set du = dist (P,u);
set ds = dist (P,spq);
A43: (((1 - Ur) * p) + (Ur * q)) - p = Ur * (q - p) by Lm1;
dist (P,u) = |.(Ur * (q - p)).| by A36, A39, A43, SPPOL_1:39
.= Ur * |.(q - p).| by A41, TOPRNS_1:7 ;
hence dist (P,u) <= dist (P,spq) by A38, A42, XREAL_1:64; :: thesis: verum
end;
thus for r being Real st r > 0 holds
ex u being Point of (Euclid n) st
( u in A /\ (halfline (p,q)) & dist (spq,u) < r ) by A15; :: thesis: verum