let n be Nat; for p, q being Point of (TOP-REAL n)
for A being convex Subset of (TOP-REAL n) st A is closed & p in Int A & p <> q & A /\ (halfline (p,q)) is bounded holds
ex u being Point of (TOP-REAL n) st (Fr A) /\ (halfline (p,q)) = {u}
let p, q be Point of (TOP-REAL n); for A being convex Subset of (TOP-REAL n) st A is closed & p in Int A & p <> q & A /\ (halfline (p,q)) is bounded holds
ex u being Point of (TOP-REAL n) st (Fr A) /\ (halfline (p,q)) = {u}
set TRn = TOP-REAL n;
set En = Euclid n;
let A be convex Subset of (TOP-REAL n); ( A is closed & p in Int A & p <> q & A /\ (halfline (p,q)) is bounded implies ex u being Point of (TOP-REAL n) st (Fr A) /\ (halfline (p,q)) = {u} )
assume that
A1:
A is closed
and
A2:
p in Int A
and
A3:
p <> q
and
A4:
A /\ (halfline (p,q)) is bounded
; ex u being Point of (TOP-REAL n) st (Fr A) /\ (halfline (p,q)) = {u}
reconsider P = p, Q = q as Point of (Euclid n) by EUCLID:67;
A5:
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n)
by EUCLID:def 8;
then reconsider I = Int A as Subset of (TopSpaceMetr (Euclid n)) ;
Int A in the topology of (TopSpaceMetr (Euclid n))
by A5, PRE_TOPC:def 2;
then
I is open
by PRE_TOPC:def 2;
then consider r being Real such that
A6:
r > 0
and
A7:
Ball (P,r) c= I
by A2, TOPMETR:15;
dist (P,P) < r
by A6, METRIC_1:1;
then A8:
P in Ball (P,r)
by METRIC_1:11;
set H = halfline (p,q);
reconsider AH = A /\ (halfline (p,q)) as bounded Subset of (Euclid n) by A4, JORDAN2C:11;
A9:
Int A c= A
by TOPS_1:16;
then consider W being Point of (Euclid n) such that
A10:
W in (Fr A) /\ (halfline (p,q))
and
A11:
for u, P being Point of (Euclid n) st P = p & u in AH holds
dist (P,u) <= dist (P,W)
and
for r being Real st r > 0 holds
ex u being Point of (Euclid n) st
( u in AH & dist (W,u) < r )
by A2, A3, A4, Lm3;
reconsider w = W as Point of (TOP-REAL n) by EUCLID:67;
A12:
W in Fr A
by A10, XBOOLE_0:def 4;
W in halfline (p,q)
by A10, XBOOLE_0:def 4;
then consider Wr being Real such that
A13:
W = ((1 - Wr) * p) + (Wr * q)
and
A14:
Wr >= 0
;
A15:
Fr A c= A
by A1, TOPS_1:35;
A16:
Fr A misses Ball (P,r)
by A7, TOPS_1:39, XBOOLE_1:63;
(Fr A) /\ (halfline (p,q)) = {W}
proof
assume
(Fr A) /\ (halfline (p,q)) <> {W}
;
contradiction
then consider u being
object such that A17:
u in (Fr A) /\ (halfline (p,q))
and A18:
u <> W
by A10, ZFMISC_1:35;
reconsider u =
u as
Point of
(TOP-REAL n) by A17;
A19:
u in halfline (
p,
q)
by A17, XBOOLE_0:def 4;
then consider Ur being
Real such that A20:
u = ((1 - Ur) * p) + (Ur * q)
and A21:
Ur >= 0
;
A22:
|.Ur.| = Ur
by A21, ABSVALUE:def 1;
reconsider U =
u as
Element of
(Euclid n) by EUCLID:67;
(((1 - Ur) * p) + (Ur * q)) - p = Ur * (q - p)
by Lm1;
then A23:
dist (
U,
P) =
|.(Ur * (q - p)).|
by A20, SPPOL_1:39
.=
Ur * |.(q - p).|
by A22, TOPRNS_1:7
;
set R =
(r * (Wr - Ur)) / Wr;
reconsider b =
Ball (
U,
((r * (Wr - Ur)) / Wr)) as
Subset of
(TopSpaceMetr (Euclid n)) by A5, EUCLID:67;
set x =
(Wr - Ur) / Wr;
b is
open
by TOPMETR:14;
then
b in the
topology of
(TOP-REAL n)
by A5, PRE_TOPC:def 2;
then reconsider B =
b as
open Subset of
(TOP-REAL n) by PRE_TOPC:def 2;
A24:
|.Wr.| = Wr
by A14, ABSVALUE:def 1;
(((1 - Wr) * p) + (Wr * q)) - p = Wr * (q - p)
by Lm1;
then A25:
dist (
W,
P) =
|.(Wr * (q - p)).|
by A13, SPPOL_1:39
.=
Wr * |.(q - p).|
by A24, TOPRNS_1:7
;
A26:
u in Fr A
by A17, XBOOLE_0:def 4;
then A27:
u in AH
by A15, A19, XBOOLE_0:def 4;
P <> W
by A16, A8, A12, XBOOLE_0:3;
then A28:
Wr > 0
by A25, METRIC_1:7;
then A29: 1
- ((Wr - Ur) / Wr) =
(Wr / Wr) - ((Wr - Ur) / Wr)
by XCMPLX_1:60
.=
Ur / Wr
;
P <> u
by A16, A8, A26, XBOOLE_0:3;
then
Ur > 0
by A23, METRIC_1:7;
then
1
- ((Wr - Ur) / Wr) >= ((Wr - Ur) / Wr) - ((Wr - Ur) / Wr)
by A28, A29;
then A30:
(
(Wr - Ur) / Wr in REAL &
(Wr - Ur) / Wr <= 1 )
by XREAL_0:def 1, XREAL_1:6;
A31:
((1 - Wr) * p) + (Wr * q) = (Wr * (q - p)) + p
by Th1;
A32:
((1 - Ur) * p) + (Ur * q) = p + (Ur * (q - p))
by Th1;
then (((1 - Wr) * p) + (Wr * q)) - (((1 - Ur) * p) + (Ur * q)) =
((p + (Wr * (q - p))) - p) - (Ur * (q - p))
by A31, RLVECT_1:27
.=
((Wr * (q - p)) + (p - p)) - (Ur * (q - p))
by RLVECT_1:def 3
.=
((Wr * (q - p)) + (0. (TOP-REAL n))) - (Ur * (q - p))
by RLVECT_1:5
.=
(Wr * (q - p)) - (Ur * (q - p))
.=
(Wr - Ur) * (q - p)
by RLVECT_1:35
;
then A33:
dist (
U,
W) =
|.((Wr - Ur) * (q - p)).|
by A13, A20, SPPOL_1:39
.=
|.(Wr - Ur).| * |.(q - p).|
by TOPRNS_1:7
;
dist (
U,
W)
> 0
by A18, METRIC_1:7;
then
|.(q - p).| > 0
by A33, XREAL_1:134;
then
Ur <= Wr
by A11, A23, A25, A27, XREAL_1:68;
then
Wr - Ur >= 0
by XREAL_1:48;
then A34:
|.(Wr - Ur).| = Wr - Ur
by ABSVALUE:def 1;
then A35:
Wr - Ur > 0
by A18, A33, METRIC_1:7;
dist (
U,
U)
= 0
by METRIC_1:1;
then
U in B
by A6, A28, A35, METRIC_1:11;
then
B \ A <> {}
by A26, TOPGEN_1:9;
then consider t being
object such that A36:
t in B \ A
by XBOOLE_0:def 1;
A37:
t in B
by A36, XBOOLE_0:def 5;
reconsider t =
t as
Point of
(TOP-REAL n) by A36;
set z =
p + ((Wr / (Wr - Ur)) * (t - u));
reconsider Z =
p + ((Wr / (Wr - Ur)) * (t - u)) as
Point of
(Euclid n) by EUCLID:67;
reconsider T =
t as
Point of
(Euclid n) by EUCLID:67;
A38:
dist (
U,
T)
= |.(u - t).|
by SPPOL_1:39;
A39:
(Wr / (Wr - Ur)) * ((r * (Wr - Ur)) / Wr) =
(((Wr / Wr) * (Wr - Ur)) / (Wr - Ur)) * r
.=
((Wr - Ur) / (Wr - Ur)) * r
by A28, XCMPLX_1:88
.=
r
by A35, XCMPLX_1:88
;
|.(- Wr).| = - (- Wr)
by A28, ABSVALUE:def 1;
then A40:
(
(- Wr) / (Wr - Ur) in REAL &
|.((- Wr) / (Wr - Ur)).| = Wr / (Wr - Ur) )
by A34, COMPLEX1:67, XREAL_0:def 1;
A41:
(Ur / Wr) * (Wr * (q - p)) =
((Ur / Wr) * Wr) * (q - p)
by RLVECT_1:def 7
.=
((Wr / Wr) * Ur) * (q - p)
.=
Ur * (q - p)
by A28, XCMPLX_1:88
;
p - (p + ((Wr / (Wr - Ur)) * (t - u))) =
(p - p) - ((Wr / (Wr - Ur)) * (t - u))
by RLVECT_1:27
.=
(0. (TOP-REAL n)) - ((Wr / (Wr - Ur)) * (t - u))
by RLVECT_1:15
.=
- ((Wr / (Wr - Ur)) * (t - u))
.=
(- 1) * ((Wr / (Wr - Ur)) * (t - u))
by RLVECT_1:16
.=
((- 1) * (Wr / (Wr - Ur))) * (t - u)
by RLVECT_1:def 7
.=
((- Wr) / (Wr - Ur)) * (t - u)
;
then A42:
dist (
P,
Z) =
|.(((- Wr) / (Wr - Ur)) * (t - u)).|
by SPPOL_1:39
.=
(Wr / (Wr - Ur)) * |.(t - u).|
by A40, TOPRNS_1:7
;
dist (
U,
T)
< (r * (Wr - Ur)) / Wr
by A37, METRIC_1:11;
then
(Wr / (Wr - Ur)) * |.(u - t).| < r
by A28, A35, A38, A39, XREAL_1:68;
then
dist (
P,
Z)
< r
by A38, A42, SPPOL_1:39;
then
Z in Ball (
P,
r)
by METRIC_1:11;
then A43:
Z in I
by A7;
((Wr - Ur) / Wr) * ((Wr / (Wr - Ur)) * (t - u)) =
(((Wr - Ur) / Wr) * (Wr / (Wr - Ur))) * (t - u)
by RLVECT_1:def 7
.=
((((Wr - Ur) / (Wr - Ur)) * Wr) / Wr) * (t - u)
.=
(Wr / Wr) * (t - u)
by A35, XCMPLX_1:88
.=
1
* (t - u)
by A28, XCMPLX_1:60
.=
t - u
by RLVECT_1:def 8
;
then
((Wr - Ur) / Wr) * (p + ((Wr / (Wr - Ur)) * (t - u))) = (((Wr - Ur) / Wr) * p) + (t - u)
by RLVECT_1:def 5;
then (((Wr - Ur) / Wr) * (p + ((Wr / (Wr - Ur)) * (t - u)))) + ((1 - ((Wr - Ur) / Wr)) * w) =
((t - u) + (((Wr - Ur) / Wr) * p)) + (((1 - ((Wr - Ur) / Wr)) * p) + (Ur * (q - p)))
by A13, A29, A31, A41, RLVECT_1:def 5
.=
(((t - u) + (((Wr - Ur) / Wr) * p)) + ((1 - ((Wr - Ur) / Wr)) * p)) + (Ur * (q - p))
by RLVECT_1:def 3
.=
((t - u) + ((((Wr - Ur) / Wr) * p) + ((1 - ((Wr - Ur) / Wr)) * p))) + (Ur * (q - p))
by RLVECT_1:def 3
.=
((t - u) + ((((Wr - Ur) / Wr) + (1 - ((Wr - Ur) / Wr))) * p)) + (Ur * (q - p))
by RLVECT_1:def 6
.=
((t - u) + p) + (Ur * (q - p))
by RLVECT_1:def 8
.=
(t - u) + u
by A20, A32, RLVECT_1:def 3
.=
t - (u - u)
by RLVECT_1:29
.=
t - (0. (TOP-REAL n))
by RLVECT_1:15
.=
t
;
then
t in A
by A15, A9, A12, A28, A30, A35, A43, RLTOPSP1:def 1;
hence
contradiction
by A36, XBOOLE_0:def 5;
verum
end;
hence
ex u being Point of (TOP-REAL n) st (Fr A) /\ (halfline (p,q)) = {u}
by A10; verum