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}
A5:
n in NAT
by ORDINAL1:def 12;
reconsider P = p, Q = q as Point of (Euclid n) by EUCLID:67;
A6:
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 A6, PRE_TOPC:def 2;
then
I is open
by PRE_TOPC:def 2;
then consider r being real number such that
A7:
r > 0
and
A8:
Ball (P,r) c= I
by A2, TOPMETR:15;
dist (P,P) < r
by A7, METRIC_1:1;
then A9:
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:def 1;
A10:
Int A c= A
by TOPS_1:16;
then consider W being Point of (Euclid n) such that
A11:
W in (Fr A) /\ (halfline (p,q))
and
A12:
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 number 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;
A13:
W in Fr A
by A11, XBOOLE_0:def 4;
W in halfline (p,q)
by A11, XBOOLE_0:def 4;
then consider Wr being real number such that
A14:
W = ((1 - Wr) * p) + (Wr * q)
and
A15:
Wr >= 0
by A5, TOPREAL9:26;
A16:
Fr A c= A
by A1, TOPS_1:35;
A17:
Fr A misses Ball (P,r)
by A8, 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
set such that A18:
u in (Fr A) /\ (halfline (p,q))
and A19:
u <> W
by A11, ZFMISC_1:35;
reconsider u =
u as
Point of
(TOP-REAL n) by A18;
A20:
u in halfline (
p,
q)
by A18, XBOOLE_0:def 4;
then consider Ur being
real number such that A21:
u = ((1 - Ur) * p) + (Ur * q)
and A22:
Ur >= 0
by A5, TOPREAL9:26;
A23:
abs Ur = Ur
by A22, ABSVALUE:def 1;
reconsider U =
u as
Element of
(Euclid n) by EUCLID:67;
A24:
Wr - Ur in REAL
by XREAL_0:def 1;
(((1 - Ur) * p) + (Ur * q)) - p = Ur * (q - p)
by Lm1;
then A25:
dist (
U,
P) =
|.(Ur * (q - p)).|
by A5, A21, SPPOL_1:39
.=
Ur * |.(q - p).|
by A5, A23, TOPRNS_1:7
;
set R =
(r * (Wr - Ur)) / Wr;
reconsider b =
Ball (
U,
((r * (Wr - Ur)) / Wr)) as
Subset of
(TopSpaceMetr (Euclid n)) by A6, EUCLID:67;
set x =
(Wr - Ur) / Wr;
b is
open
by TOPMETR:14;
then
b in the
topology of
(TOP-REAL n)
by A6, PRE_TOPC:def 2;
then reconsider B =
b as
open Subset of
(TOP-REAL n) by PRE_TOPC:def 2;
A26:
abs Wr = Wr
by A15, ABSVALUE:def 1;
(((1 - Wr) * p) + (Wr * q)) - p = Wr * (q - p)
by Lm1;
then A27:
dist (
W,
P) =
|.(Wr * (q - p)).|
by A5, A14, SPPOL_1:39
.=
Wr * |.(q - p).|
by A5, A26, TOPRNS_1:7
;
A28:
u in Fr A
by A18, XBOOLE_0:def 4;
then A29:
u in AH
by A16, A20, XBOOLE_0:def 4;
P <> W
by A17, A9, A13, XBOOLE_0:3;
then A30:
Wr > 0
by A27, METRIC_1:7;
then A31: 1
- ((Wr - Ur) / Wr) =
(Wr / Wr) - ((Wr - Ur) / Wr)
by XCMPLX_1:60
.=
Ur / Wr
;
P <> u
by A17, A9, A28, XBOOLE_0:3;
then
Ur > 0
by A25, METRIC_1:7;
then
1
- ((Wr - Ur) / Wr) >= ((Wr - Ur) / Wr) - ((Wr - Ur) / Wr)
by A30, A31;
then A32:
(
(Wr - Ur) / Wr in REAL &
(Wr - Ur) / Wr <= 1 )
by XREAL_0:def 1, XREAL_1:6;
A33:
((1 - Wr) * p) + (Wr * q) = (Wr * (q - p)) + p
by Th1;
A34:
((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 A33, RLVECT_1:27
.=
((Wr * (q - p)) + (p - p)) - (Ur * (q - p))
by EUCLID:45
.=
((Wr * (q - p)) + (0. (TOP-REAL n))) - (Ur * (q - p))
by EUCLID:42
.=
(Wr * (q - p)) - (Ur * (q - p))
by RLVECT_1:def 4
.=
(Wr - Ur) * (q - p)
by EUCLID:50
;
then A35:
dist (
U,
W) =
|.((Wr - Ur) * (q - p)).|
by A5, A14, A21, SPPOL_1:39
.=
(abs (Wr - Ur)) * |.(q - p).|
by A5, A24, TOPRNS_1:7
;
dist (
U,
W)
> 0
by A19, METRIC_1:7;
then
|.(q - p).| > 0
by A35, XREAL_1:134;
then
Ur <= Wr
by A12, A25, A27, A29, XREAL_1:68;
then
Wr - Ur >= 0
by XREAL_1:48;
then A36:
abs (Wr - Ur) = Wr - Ur
by ABSVALUE:def 1;
then A37:
Wr - Ur > 0
by A19, A35, METRIC_1:7;
dist (
U,
U)
= 0
by METRIC_1:1;
then
U in B
by A7, A30, A37, METRIC_1:11;
then
B \ A <> {}
by A28, TOPGEN_1:9;
then consider t being
set such that A38:
t in B \ A
by XBOOLE_0:def 1;
A39:
t in B
by A38, XBOOLE_0:def 5;
reconsider t =
t as
Point of
(TOP-REAL n) by A38;
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;
A40:
dist (
U,
T)
= |.(u - t).|
by A5, SPPOL_1:39;
A41:
(Wr / (Wr - Ur)) * ((r * (Wr - Ur)) / Wr) =
(((Wr / Wr) * (Wr - Ur)) / (Wr - Ur)) * r
.=
((Wr - Ur) / (Wr - Ur)) * r
by A30, XCMPLX_1:88
.=
r
by A37, XCMPLX_1:88
;
abs (- Wr) = - (- Wr)
by A30, ABSVALUE:def 1;
then A42:
(
(- Wr) / (Wr - Ur) in REAL &
abs ((- Wr) / (Wr - Ur)) = Wr / (Wr - Ur) )
by A36, COMPLEX1:67, XREAL_0:def 1;
A43:
(Ur / Wr) * (Wr * (q - p)) =
((Ur / Wr) * Wr) * (q - p)
by RLVECT_1:def 7
.=
((Wr / Wr) * Ur) * (q - p)
.=
Ur * (q - p)
by A30, 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))
by RLVECT_1:14
.=
(- 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 A44:
dist (
P,
Z) =
|.(((- Wr) / (Wr - Ur)) * (t - u)).|
by A5, SPPOL_1:39
.=
(Wr / (Wr - Ur)) * |.(t - u).|
by A5, A42, TOPRNS_1:7
;
dist (
U,
T)
< (r * (Wr - Ur)) / Wr
by A39, METRIC_1:11;
then
(Wr / (Wr - Ur)) * |.(u - t).| < r
by A30, A37, A40, A41, XREAL_1:68;
then
dist (
P,
Z)
< r
by A5, A40, A44, SPPOL_1:39;
then
Z in Ball (
P,
r)
by METRIC_1:11;
then A45:
Z in I
by A8;
((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 A37, XCMPLX_1:88
.=
1
* (t - u)
by A30, 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 A14, A31, A33, A43, 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 A21, A34, RLVECT_1:def 3
.=
t - (u - u)
by RLVECT_1:29
.=
t - (0. (TOP-REAL n))
by RLVECT_1:15
.=
t
by RLVECT_1:13
;
then
t in A
by A16, A10, A13, A30, A32, A37, A45, RLTOPSP1:def 1;
hence
contradiction
by A38, XBOOLE_0:def 5;
verum
end;
hence
ex u being Point of (TOP-REAL n) st (Fr A) /\ (halfline (p,q)) = {u}
by A11; verum