:: Intersections of Intervals and Balls in TOP-REAL n
:: by Artur Korni{\l}owicz and Yasunari Shidama
::
:: Received May 10, 2004
:: Copyright (c) 2004-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, PRE_TOPC, EUCLID, ARYTM_1, ARYTM_3, SUPINF_2,
XBOOLE_0, JORDAN2C, RELAT_1, CARD_1, VALUED_0, FINSEQ_1, COMPLEX1,
SQUARE_1, CARD_3, RVSUM_1, XXREAL_0, METRIC_1, NAT_1, TARSKI, STRUCT_0,
REAL_1, RCOMP_1, XXREAL_2, CONVEX1, RLTOPSP1, FUNCT_1, UNIALG_1,
MSSUBFAM, FUNCOP_1, ORDINAL2, JGRAPH_2, MCART_1, PROB_1, FINSEQ_2,
FUNCT_3, POLYEQ_1, JGRAPH_6, XCMPLX_0, RLVECT_1, INCSP_1, PENCIL_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS,
XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, REAL_1, FINSEQ_1, FINSEQ_2,
RVSUM_1, VALUED_0, SQUARE_1, QUIN_1, POLYEQ_1, STRUCT_0, PRE_TOPC,
METRIC_1, TBSP_1, RLVECT_1, RLTOPSP1, EUCLID, JGRAPH_2, JGRAPH_6,
VECTSP_1;
constructors REAL_1, SQUARE_1, BINOP_2, COMPLEX1, QUIN_1, FINSEQOP, POLYEQ_1,
BORSUK_1, TBSP_1, MONOID_0, JGRAPH_2, JGRAPH_6, CONVEX1, GRCAT_1;
registrations XBOOLE_0, XXREAL_0, XREAL_0, SQUARE_1, STRUCT_0, MONOID_0,
EUCLID, TOPALG_2, VALUED_0, FINSEQ_1, RELAT_1, PRE_TOPC, TBSP_1,
JORDAN2C, QUIN_1, ORDINAL1, RLTOPSP1, CARD_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
definitions TARSKI, XBOOLE_0, RLTOPSP1, JORDAN1, VECTSP_1;
equalities RLTOPSP1, SQUARE_1, EUCLID, XCMPLX_0, ALGSTR_0, STRUCT_0;
expansions TARSKI, XBOOLE_0, RLTOPSP1;
theorems JGRAPH_6, TOPRNS_1, TARSKI, SUBSET_1, FUNCT_2, EUCLID, JGRAPH_2,
XBOOLE_1, XBOOLE_0, FUNCOP_1, JORDAN2C, JORDAN1, SQUARE_1, XCMPLX_1,
ABSVALUE, JGRAPH_1, QUIN_1, POLYEQ_1, TOPREAL3, METRIC_1, TOPREAL6,
RVSUM_1, EUCLID_2, GOBOARD6, REVROT_1, ENUMSET1, COMPLEX1, XREAL_1,
XXREAL_0, RLTOPSP1, RLVECT_1, VECTSP_1, RLVECT_4;
begin :: Preliminaries
reserve n for Nat,
a, b, r, w for Real,
x, y, z for Point of TOP-REAL n,
e for Point of Euclid n;
::$CT 2
theorem Th1:
n is non zero implies x <> x + 1.REAL n
proof
A1: 0.REAL n = 0.TOP-REAL n & x = x + 0.TOP-REAL n by EUCLID:66,RLVECT_1:4;
assume that
A2: n is non zero and
A3: x = x + 1.REAL n;
0.REAL n <> 1.REAL n by A2,REVROT_1:19;
hence thesis by A1,A3,RLVECT_1:8;
end;
theorem Th2:
for V being RealLinearSpace, y,z being Point of V
for x being object holds x = (1-r)*y + r*z implies (x = y iff r = 0
or y = z) & (x = z iff r = 1 or y = z)
proof
let V be RealLinearSpace, y,z be Point of V;
let x be object;
assume
A1: x = (1-r)*y + r*z;
hereby
assume x = y;
then 0.V = (1-r)*y + r*z - y by A1,RLVECT_1:5
.= (1-r)*y - y + r*z by RLVECT_1:def 3
.= (1-r)*y - 1 * y + r*z by RLVECT_1:def 8
.= (1-r-1)*y + r*z by RLVECT_1:35
.= r*z - r*y by RLVECT_1:79
.= r*(z-y) by RLVECT_1:34;
then r = 0 or z-y = 0.V by RLVECT_1:11;
hence r = 0 or y = z by RLVECT_1:21;
end;
hereby
assume
A2: r = 0 or y = z;
per cases by A2;
suppose
r = 0;
hence x = y + 0 * z by A1,RLVECT_1:def 8
.= y + 0.V by RLVECT_1:10
.= y by RLVECT_1:4;
end;
suppose
z = y;
hence x = (1-r+r)*y by A1,RLVECT_1:def 6
.= y by RLVECT_1:def 8;
end;
end;
hereby
assume x = z;
then 0.V = (1-r)*y + r*z - z by A1,RLVECT_1:5
.= (1-r)*y + (r*z - z) by RLVECT_1:def 3
.= (1-r)*y + (r*z + (-1)*z) by RLVECT_1:16
.= (1-r)*y + (-1+r)*z by RLVECT_1:def 6
.= (1-r)*y + (-(1-r))*z
.= (1-r)*y - (1-r)*z by RLVECT_1:79
.= (1-r)*(y-z) by RLVECT_1:34;
then 1-r+r = 0+r or y-z = 0.V by RLVECT_1:11;
hence r = 1 or y = z by RLVECT_1:21;
end;
assume
A3: r = 1 or y = z;
per cases by A3;
suppose
r = 1;
hence x = 0.V + 1 * z by A1,RLVECT_1:10
.= 1 * z by RLVECT_1:4
.= z by RLVECT_1:def 8;
end;
suppose
y = z;
hence x = (1-r+r)*z by A1,RLVECT_1:def 6
.= z by RLVECT_1:def 8;
end;
end;
theorem Th3:
for f being real-valued FinSequence holds |.f.|^2 = Sum sqr f
proof
let f be real-valued FinSequence;
Sum sqr f >= 0 by RVSUM_1:86;
hence thesis by SQUARE_1:def 2;
end;
theorem Th4:
for M being non empty MetrSpace, z1, z2, z3 being Point of M st
z1 <> z2 & z1 in cl_Ball(z3,r) & z2 in cl_Ball(z3,r) holds r > 0
proof
let M be non empty MetrSpace, z1, z2, z3 be Point of M such that
A1: z1 <> z2 and
A2: z1 in cl_Ball(z3,r) and
A3: z2 in cl_Ball(z3,r);
now
assume r = 0;
then
A4: cl_Ball(z3,r) = {z3} by TOPREAL6:56;
then z1 = z3 by A2,TARSKI:def 1;
hence contradiction by A1,A3,A4,TARSKI:def 1;
end;
hence thesis by A2,TOPREAL6:55;
end;
begin :: Subsets of TOP-REAL n
definition
let n be Nat, x be Point of TOP-REAL n, r be Real;
func Ball(x,r) -> Subset of TOP-REAL n equals
{p where p is Point of
TOP-REAL n: |. p-x .| < r};
coherence
proof
{p where p is Point of TOP-REAL n: |. p-x .| < r} c= the carrier of
TOP-REAL n
proof
let q be object;
assume q in {p where p is Point of TOP-REAL n: |. p-x .| < r};
then ex p being Point of TOP-REAL n st q = p & |. p-x .| < r;
hence thesis;
end;
hence thesis;
end;
func cl_Ball(x,r) -> Subset of TOP-REAL n equals
{p where p is Point of
TOP-REAL n: |. p-x .| <= r};
coherence
proof
{p where p is Point of TOP-REAL n: |. p-x .| <= r} c= the carrier of
TOP-REAL n
proof
let q be object;
assume q in {p where p is Point of TOP-REAL n: |. p-x .| <= r};
then ex p being Point of TOP-REAL n st q = p & |. p-x .| <= r;
hence thesis;
end;
hence thesis;
end;
func Sphere(x,r) -> Subset of TOP-REAL n equals
{p where p is Point of
TOP-REAL n: |. p-x .| = r};
coherence
proof
{p where p is Point of TOP-REAL n: |. p-x .| = r} c= the carrier of
TOP-REAL n
proof
let q be object;
assume q in {p where p is Point of TOP-REAL n: |. p-x .| = r};
then ex p being Point of TOP-REAL n st q = p & |. p-x .| = r;
hence thesis;
end;
hence thesis;
end;
end;
theorem Th5:
y in Ball(x,r) iff |. y-x .| < r
proof
hereby
assume y in Ball(x,r);
then ex p being Point of TOP-REAL n st y = p & |. p-x .| < r;
hence |. y-x .| < r;
end;
thus thesis;
end;
theorem Th6:
y in cl_Ball(x,r) iff |. y-x .| <= r
proof
hereby
assume y in cl_Ball(x,r);
then ex p being Point of TOP-REAL n st y = p & |. p-x .| <= r;
hence |. y-x .| <= r;
end;
thus thesis;
end;
theorem Th7:
y in Sphere(x,r) iff |. y-x .| = r
proof
hereby
assume y in Sphere(x,r);
then ex p being Point of TOP-REAL n st y = p & |. p-x .| = r;
hence |. y-x .| = r;
end;
thus thesis;
end;
theorem
y in Ball(0.TOP-REAL n,r) implies |.y.| < r
proof
assume y in Ball(0.TOP-REAL n,r);
then |. y-0.TOP-REAL n .| < r by Th5;
hence thesis by RLVECT_1:13;
end;
theorem
y in cl_Ball(0.TOP-REAL n,r) implies |.y.| <= r
proof
assume y in cl_Ball(0.TOP-REAL n,r);
then |. y-0.TOP-REAL n .| <= r by Th6;
hence thesis by RLVECT_1:13;
end;
theorem
y in Sphere(0.TOP-REAL n,r) implies |.y.| = r
proof
assume y in Sphere(0.TOP-REAL n,r);
then |. y-0.TOP-REAL n .| = r by Th7;
hence thesis by RLVECT_1:13;
end;
theorem Th11:
x = e implies Ball(e,r) = Ball(x,r)
proof
assume
A1: x = e;
hereby
let q be object;
assume
A2: q in Ball(e,r);
then reconsider f = q as Point of Euclid n;
reconsider p = f as Point of TOP-REAL n by TOPREAL3:8;
dist(f,e) < r by A2,METRIC_1:11;
then |. p-x .| < r by A1,JGRAPH_1:28;
hence q in Ball(x,r);
end;
let q be object;
assume
A3: q in Ball(x,r);
then reconsider q as Point of TOP-REAL n;
reconsider f = q as Point of Euclid n by TOPREAL3:8;
|. q-x .| < r by A3,Th5;
then dist(f,e) < r by A1,JGRAPH_1:28;
hence thesis by METRIC_1:11;
end;
theorem Th12:
x = e implies cl_Ball(e,r) = cl_Ball(x,r)
proof
assume
A1: x = e;
hereby
let q be object;
assume
A2: q in cl_Ball(e,r);
then reconsider f = q as Point of Euclid n;
reconsider p = f as Point of TOP-REAL n by TOPREAL3:8;
dist(f,e) <= r by A2,METRIC_1:12;
then |. p-x .| <= r by A1,JGRAPH_1:28;
hence q in cl_Ball(x,r);
end;
let q be object;
assume
A3: q in cl_Ball(x,r);
then reconsider q as Point of TOP-REAL n;
reconsider f = q as Point of Euclid n by TOPREAL3:8;
|. q-x .| <= r by A3,Th6;
then dist(f,e) <= r by A1,JGRAPH_1:28;
hence thesis by METRIC_1:12;
end;
theorem Th13:
x = e implies Sphere(e,r) = Sphere(x,r)
proof
assume
A1: x = e;
hereby
let q be object;
assume
A2: q in Sphere(e,r);
then reconsider f = q as Point of Euclid n;
reconsider p = f as Point of TOP-REAL n by TOPREAL3:8;
dist(f,e) = r by A2,METRIC_1:13;
then |. p-x .| = r by A1,JGRAPH_1:28;
hence q in Sphere(x,r);
end;
let q be object;
assume
A3: q in Sphere(x,r);
then reconsider q as Point of TOP-REAL n;
reconsider f = q as Point of Euclid n by TOPREAL3:8;
|. q-x .| = r by A3,Th7;
then dist(f,e) = r by A1,JGRAPH_1:28;
hence thesis by METRIC_1:13;
end;
theorem
Ball(x,r) c= cl_Ball(x,r)
proof
reconsider e = x as Point of Euclid n by TOPREAL3:8;
Ball(x,r) = Ball(e,r) & cl_Ball(x,r) = cl_Ball(e,r) by Th11,Th12;
hence thesis by METRIC_1:14;
end;
theorem Th15:
Sphere(x,r) c= cl_Ball(x,r)
proof
reconsider e = x as Point of Euclid n by TOPREAL3:8;
Sphere(x,r) = Sphere(e,r) & cl_Ball(x,r) = cl_Ball(e,r) by Th12,Th13;
hence thesis by METRIC_1:15;
end;
theorem Th16:
Ball(x,r) \/ Sphere(x,r) = cl_Ball(x,r)
proof
reconsider e = x as Point of Euclid n by TOPREAL3:8;
A1: cl_Ball(x,r) = cl_Ball(e,r) by Th12;
Sphere(x,r) = Sphere(e,r) & Ball(x,r) = Ball(e,r) by Th11,Th13;
hence thesis by A1,METRIC_1:16;
end;
theorem Th17:
Ball(x,r) misses Sphere(x,r)
proof
assume not thesis;
then consider q being object such that
A1: q in Ball(x,r) and
A2: q in Sphere(x,r) by XBOOLE_0:3;
reconsider q as Point of TOP-REAL n by A1;
|. q - x .| = r by A2,Th7;
hence thesis by A1,Th5;
end;
registration
let n be Nat, x be Point of TOP-REAL n;
let r be non positive Real;
cluster Ball(x,r) -> empty;
coherence
proof
assume not thesis;
then consider y being Point of TOP-REAL n such that
A1: y in Ball(x,r);
|. y - x .| < r by A1,Th5;
hence contradiction;
end;
end;
registration
let n be Nat, x be Point of TOP-REAL n;
let r be positive Real;
cluster Ball(x,r) -> non empty;
coherence
proof
reconsider e = x as Point of Euclid n by TOPREAL3:8;
Ball(x,r) = Ball(e,r) by Th11;
hence thesis by GOBOARD6:1;
end;
end;
theorem
Ball(x,r) is non empty implies r > 0;
theorem
Ball(x,r) is empty implies r <= 0;
registration
let n be Nat, x be Point of TOP-REAL n;
let r be negative Real;
cluster cl_Ball(x,r) -> empty;
coherence
proof
assume not thesis;
then consider y being Point of TOP-REAL n such that
A1: y in cl_Ball(x,r);
|. y - x .| <= r by A1,Th6;
hence contradiction;
end;
end;
registration
let n be Nat, x be Point of TOP-REAL n;
let r be non negative Real;
cluster cl_Ball(x,r) -> non empty;
coherence
proof
|. x-x .| = 0 by TOPRNS_1:28;
hence thesis by Th6;
end;
end;
theorem
cl_Ball(x,r) is non empty implies r >= 0;
theorem
cl_Ball(x,r) is empty implies r < 0;
theorem Th22:
a + b = 1 & |.a.| + |.b.| = 1 & b <> 0 & x in cl_Ball(z,r) & y
in Ball(z,r) implies a * x + b * y in Ball(z,r)
proof
assume that
A1: a + b = 1 and
A2: |.a.| + |.b.| = 1 and
A3: b <> 0 and
A4: x in cl_Ball(z,r) and
A5: y in Ball(z,r);
|. y-z .| < r by A5,Th5;
then
A6: |. z-y .| < r by TOPRNS_1:27;
|. x-z .| <= r by A4,Th6;
then 0 <= |.a.| & |. z-x .| <= r by COMPLEX1:46,TOPRNS_1:27;
then
A7: |.a.|*|. z-x .| <= |.a.|*r by XREAL_1:64;
0 < |.b.| by A3,COMPLEX1:47;
then |.b.|*|. z-y .| < |.b.|*r by A6,XREAL_1:68;
then |.a.|*|. z-x .| + |.b.|*|. z-y .| < |.a.|*r + |.b.|*r by A7,XREAL_1:8;
then a is Real & |.a.|*|. z-x .| + |.b.|*|. z-y .| < (|.a.|+|.b.|)*r;
then b is Real & |. a*(z-x) .| + |.b.|*|. z-y .| < 1 * r by A2,TOPRNS_1:7;
then
A8: |. a*(z-x) .| + |. b*(z-y) .| < r by TOPRNS_1:7;
|. a*z + b*z - (a*x + b*y) .| = |. a*z - (a*x + b*y) + b*z .| by
RLVECT_1:def 3
.= |. a*z - a*x - b*y + b*z .| by RLVECT_1:27
.= |. a*z - a*x + b*z - b*y .| by RLVECT_1:def 3
.= |. a*z - a*x + (b*z - b*y) .| by RLVECT_1:def 3
.= |. a*(z-x) + (b*z - b*y) .| by RLVECT_1:34
.= |. a*(z-x) + b*(z-y) .| by RLVECT_1:34;
then |. a*z + b*z - (a*x + b*y) .| <= |. a*(z-x) .| + |. b*(z-y) .| by
TOPRNS_1:29;
then |. a*z + b*z - (a*x + b*y) .| < r by A8,XXREAL_0:2;
then
A9: |. a*x + b*y - (a*z + b*z) .| < r by TOPRNS_1:27;
a*z + b*z = (a+b)*z by RLVECT_1:def 6
.= z by A1,RLVECT_1:def 8;
hence thesis by A9;
end;
registration
let n be Nat, x be Point of TOP-REAL n;
let r;
cluster Ball(x,r) -> open;
coherence
proof
reconsider e = x as Point of Euclid n by TOPREAL3:8;
Ball(e,r) = Ball(x,r) by Th11;
hence thesis by GOBOARD6:3;
end;
cluster cl_Ball(x,r) -> closed;
coherence
proof
reconsider e = x as Point of Euclid n by TOPREAL3:8;
cl_Ball(e,r) is bounded & cl_Ball(e,r) = cl_Ball(x,r)
by Th12,TOPREAL6:59;
hence thesis by TOPREAL6:58;
end;
cluster Sphere(x,r) -> closed;
coherence
proof
reconsider e = x as Point of Euclid n by TOPREAL3:8;
Sphere(e,r) is bounded & Sphere(e,r) = Sphere(x,r) by Th13,TOPREAL6:62;
hence thesis by TOPREAL6:61;
end;
end;
registration
let n,x,r;
cluster Ball(x,r) -> bounded;
coherence
proof
reconsider e = x as Point of Euclid n by TOPREAL3:8;
Ball(e,r) = Ball(x,r) by Th11;
hence thesis by JORDAN2C:11;
end;
cluster cl_Ball(x,r) -> bounded;
coherence
proof
reconsider e = x as Point of Euclid n by TOPREAL3:8;
cl_Ball(e,r) is bounded & cl_Ball(e,r) = cl_Ball(x,r) by Th12,TOPREAL6:59;
hence thesis by JORDAN2C:11;
end;
cluster Sphere(x,r) -> bounded;
coherence
proof
reconsider e = x as Point of Euclid n by TOPREAL3:8;
Sphere(e,r) is bounded & Sphere(e,r) = Sphere(x,r) by Th13,TOPREAL6:62;
hence thesis by JORDAN2C:11;
end;
end;
Lm1: for a being Real, P being Subset of TOP-REAL n, Q being Point of
TOP-REAL n st P = {q where q is Point of TOP-REAL n: |.q - Q.| <= a} holds P is
convex
proof
let a be Real, P be Subset of TOP-REAL n, Q be Point of TOP-REAL n;
assume
A1: P = {q where q is Point of TOP-REAL n: |.q - Q.| <= a};
let p1,p2 be Point of TOP-REAL n;
assume p1 in P;
then
A2: ex q1 being Point of TOP-REAL n st q1=p1 & |.q1-Q.| <= a by A1;
assume
A3: p2 in P;
then
A4: ex q2 being Point of TOP-REAL n st q2=p2 & |.q2-Q.| <= a by A1;
let x be object;
assume
A5: x in LSeg(p1,p2);
then consider r being Real such that
A6: x = (1-r)*p1+r*p2 and
A7: 0 <= r and
A8: r <= 1;
A9: r = |.r.| by A7,ABSVALUE:def 1;
reconsider q = x as Point of TOP-REAL n by A5;
A10: |.(1-r)*(p1-Q).| = |.1-r.|*|.p1-Q.| by TOPRNS_1:7;
A11: 1-r >= 0 by A8,XREAL_1:48;
then
A12: |.1-r.| = 1-r by ABSVALUE:def 1;
per cases;
suppose
A13: 1-r > 0;
0 <= |.r.| by COMPLEX1:46;
then
A14: |.r*(p2-Q).| = |.r.|*|.p2-Q.| & |.r.|*|.p2-Q.| <= |.r.|*a by A4,TOPRNS_1:7
,XREAL_1:64;
(1-r)*Q + r*Q = 1 * Q - r*Q + r*Q by RLVECT_1:35
.= 1 * Q by RLVECT_4:1
.= Q by RLVECT_1:def 8;
then q-Q = (1-r)*p1+r*p2-(1-r)*Q-r*Q by A6,RLVECT_1:27
.= (1-r)*p1-(1-r)*Q+r*p2-r*Q by RLVECT_1:def 3
.= (1-r)*(p1-Q)+r*p2-r*Q by RLVECT_1:34
.= (1-r)*(p1-Q)+(r*p2-r*Q) by RLVECT_1:def 3
.= (1-r)*(p1-Q)+r*(p2-Q) by RLVECT_1:34;
then
A15: |.q-Q.| <= |.(1-r)*(p1-Q).| + |.r*(p2-Q).| by TOPRNS_1:29;
|.1-r.|*|.p1-Q.| <= |.1-r.|*a by A2,A12,A13,XREAL_1:64;
then |.(1-r)*(p1-Q).|+|.r*(p2-Q).| <= (1-r)*a+r*a by A9,A10,A12,A14,
XREAL_1:7;
then |.q-Q.| <= a by A15,XXREAL_0:2;
hence thesis by A1;
end;
suppose
1-r <= 0;
then 1-r+r = 0+r by A11;
hence thesis by A3,A6,Th2;
end;
end;
Lm2: for a being Real, P being Subset of TOP-REAL n, Q being Point of
TOP-REAL n st P = {q where q is Point of TOP-REAL n: |.q - Q.| < a} holds P is
convex
proof
let a be Real, P be Subset of TOP-REAL n, Q be Point of TOP-REAL n;
assume
A1: P = {q where q is Point of TOP-REAL n: |.q - Q.| < a};
reconsider e = Q as Point of Euclid n by TOPREAL3:8;
let p1,p2 be Point of TOP-REAL n;
assume
A2: p1 in P & p2 in P;
Ball(e,a) = Ball(Q,a) by Th11
.= P by A1;
hence thesis by A2,TOPREAL3:21;
end;
:: Convex subsets of TOP-REAL n
registration
let n be Nat, x be Point of TOP-REAL n;
let r;
cluster Ball(x,r) -> convex;
coherence
by Lm2;
cluster cl_Ball(x,r) -> convex;
coherence
by Lm1;
end;
definition
let n be Nat;
let f be Function of TOP-REAL n, TOP-REAL n;
attr f is homogeneous means
:Def4:
for r being Real, x being Point of TOP-REAL n holds f.(r*x) = r * f.x;
end;
registration
let n;
cluster TOP-REAL n --> 0.TOP-REAL n -> homogeneous additive;
coherence
proof
set f = TOP-REAL n --> 0.TOP-REAL n;
thus f is homogeneous
proof
let r be Real, x be Point of TOP-REAL n;
thus f.(r*x) = 0.TOP-REAL n by FUNCOP_1:7
.= r * 0.TOP-REAL n by RLVECT_1:10
.= r * f.x by FUNCOP_1:7;
end;
let x, y be Point of TOP-REAL n;
thus f.(x+y) = 0.TOP-REAL n by FUNCOP_1:7
.= 0.TOP-REAL n + 0.TOP-REAL n by RLVECT_1:4
.= f.x + 0.TOP-REAL n by FUNCOP_1:7
.= f.x + f.y by FUNCOP_1:7;
end;
end;
registration
let n;
cluster homogeneous additive continuous for
Function of TOP-REAL n, TOP-REAL n;
existence
proof
take TOP-REAL n --> 0.TOP-REAL n;
thus thesis;
end;
end;
registration
let a, c be Real;
cluster AffineMap(a,0,c,0) -> homogeneous additive;
coherence
proof
set f = AffineMap(a,0,c,0);
hereby
let r be Real, x be Point of TOP-REAL 2;
A1: (r*x)`1 = r*x`1 & (r*x)`2 = r*x`2 by TOPREAL3:4;
thus f.(r*x) = |[a*((r*x)`1)+0,c*((r*x)`2)+0]| by JGRAPH_2:def 2
.= |[r*(a*(x`1)),r*(c*(x`2))]| by A1
.= r * |[a*(x`1)+0,c*(x`2)+0]| by EUCLID:58
.= r * f.x by JGRAPH_2:def 2;
end;
let x, y be Point of TOP-REAL 2;
A2: (x+y)`1 = x`1 + y`1 & (x+y)`2 = x`2 + y`2 by TOPREAL3:2;
thus f.(x+y) = |[a*((x+y)`1)+0,c*((x+y)`2)+0]| by JGRAPH_2:def 2
.= |[a*(x`1)+a*(y`1),c*(x`2)+c*(y`2)]| by A2
.= |[a*(x`1)+0,c*(x`2)+0]| + |[a*(y`1),c*(y`2)]| by EUCLID:56
.= f.x + |[a*(y`1)+0,c*(y`2)+0]| by JGRAPH_2:def 2
.= f.x + f.y by JGRAPH_2:def 2;
end;
end;
theorem
for f being homogeneous additive Function of TOP-REAL n, TOP-REAL n, X
being convex Subset of TOP-REAL n holds f.:X is convex
proof
let f be homogeneous additive Function of TOP-REAL n, TOP-REAL n, X be
convex Subset of TOP-REAL n;
let p, q be Point of TOP-REAL n;
assume p in f.:X;
then consider p0 being Point of TOP-REAL n such that
A1: p0 in X and
A2: p = f.p0 by FUNCT_2:65;
assume q in f.:X;
then consider q0 being Point of TOP-REAL n such that
A3: q0 in X and
A4: q = f.q0 by FUNCT_2:65;
A5: LSeg(p0,q0) c= X by A1,A3,JORDAN1:def 1;
let x be object;
assume x in LSeg(p,q);
then consider l being Real such that
A6: x = (1-l)*p + l*q and
A7: 0 <= l & l <= 1;
set a = (1-l)*p0 + l*q0;
A8: a in LSeg(p0,q0) by A7;
f.a = f.((1-l)*p0) + f.(l*q0) by VECTSP_1:def 20
.= f.((1-l)*p0) + l*f.q0 by Def4
.= x by A2,A4,A6,Def4;
hence thesis by A8,A5,FUNCT_2:35;
end;
:: Halflines
reserve V for RealLinearSpace,
p,q,x for Element of V;
definition
let V,p,q;
func halfline(p,q) -> Subset of V equals
{ (1-l)*p + l*q where l is Real: 0 <= l };
coherence
proof
set X = { (1-l)*p + l*q where l is Real: 0 <= l };
X c= the carrier of V
proof
let x be object;
assume x in X;
then ex l being Real st x = (1-l)*p + l*q & 0 <= l;
hence thesis;
end;
hence thesis;
end;
end;
theorem
for x being set holds x in halfline(p,q) iff ex l being Real
st x = (1-l)*p + l*q & 0 <= l;
registration
let V, p, q;
cluster halfline(p,q) -> non empty;
coherence
proof
(1-0)*p + 0 * q in halfline(p,q);
hence thesis;
end;
end;
theorem Th25:
p in halfline(p,q)
proof
(1-0)*p + 0 * q = p + 0 * q by RLVECT_1:def 8
.= p + 0.V by RLVECT_1:10
.= p by RLVECT_1:4;
hence thesis;
end;
theorem Th26:
q in halfline(p,q)
proof
(1-1)*p + 1 * q = 0 * p + q by RLVECT_1:def 8
.= 0.V + q by RLVECT_1:10
.= q by RLVECT_1:4;
hence thesis;
end;
theorem Th27:
halfline(p,p) = {p}
proof
hereby
let d be object;
assume d in halfline(p,p);
then ex r being Real st d = (1-r)*p+r*p & 0 <= r;
then d = p by Th2;
hence d in {p} by TARSKI:def 1;
end;
let d be object;
assume d in {p};
then d = p by TARSKI:def 1;
hence thesis by Th25;
end;
theorem Th28:
x in halfline(p,q) implies halfline(p,x) c= halfline(p,q)
proof
assume x in halfline(p,q);
then consider R being Real such that
A1: x = (1-R)*p + R*q and
A2: 0 <= R;
let d be object;
assume
A3: d in halfline(p,x);
then reconsider d as Point of V;
consider r being Real such that
A4: d = (1-r)*p + r*x and
A5: 0 <= r by A3;
set o = r*R;
d = (1-r)*p + (r*((1-R)*p) + r*(R*q)) by A1,A4,RLVECT_1:def 5
.= (1-r)*p + r*((1-R)*p) + r*(R*q) by RLVECT_1:def 3
.= (1-r)*p + r*(1-R)*p + r*(R*q) by RLVECT_1:def 7
.= ((1-r) + r*(1-R))*p + r*(R*q) by RLVECT_1:def 6
.= (1-o)*p + o*q by RLVECT_1:def 7;
hence thesis by A2,A5;
end;
theorem
x in halfline(p,q) & x <> p implies halfline(p,q) = halfline(p,x)
proof
assume
A1: x in halfline(p,q);
then consider R being Real such that
A2: x = (1-R)*p + R*q and
A3: 0 <= R;
assume
A4: x <> p;
thus halfline(p,q) c= halfline(p,x)
proof
let d be object;
assume
A5: d in halfline(p,q);
then reconsider d as Point of V;
consider r being Real such that
A6: d = (1-r)*p + r*q and
A7: 0 <= r by A5;
set o = r/R;
R <> 0 by A2,A4,Th2;
then o*R = r by XCMPLX_1:87;
then d = (1-o + o*(1-R))*p + o*(R*q) by A6,RLVECT_1:def 7
.= (1-o)*p + o*(1-R)*p + o*(R*q) by RLVECT_1:def 6
.= (1-o)*p + o*((1-R)*p) + o*(R*q) by RLVECT_1:def 7
.= (1-o)*p + (o*((1-R)*p) + o*(R*q)) by RLVECT_1:def 3
.= (1-o)*p + o*((1-R)*p + R*q) by RLVECT_1:def 5;
hence thesis by A2,A3,A7;
end;
thus thesis by A1,Th28;
end;
theorem
LSeg(p,q) c= halfline(p,q)
proof
let a be object;
assume a in LSeg(p,q);
then ex r being Real st 0<=r & r<=1 & a = (1-r)*p+r*q by RLTOPSP1:76;
hence thesis;
end;
registration
let V, p, q;
cluster halfline(p,q) -> convex;
coherence
proof
let u, v be Point of V;
set P = halfline(p,q);
assume u in P;
then consider a being Real such that
A1: u = (1-a)*p+a*q and
A2: 0 <= a;
assume v in P;
then consider b being Real such that
A3: v = (1-b)*p+b*q and
A4: 0 <= b;
let x be object;
assume x in LSeg(u,v);
then consider r being Real such that
A5: 0 <= r and
A6: r <= 1 and
A7: x = (1-r)*u+r*v by RLTOPSP1:76;
set o = (1-r)*a+r*b;
A8: 1-r >= r-r by A6,XREAL_1:13;
x = (1-r)*((1-a)*p)+(1-r)*(a*q) + r*((1-b)*p+b*q) by A1,A3,A7,
RLVECT_1:def 5
.= (1-r)*((1-a)*p) + (1-r)*(a*q) + (r*((1-b)*p) + r*(b*q)) by
RLVECT_1:def 5
.= (1-r)*((1-a)*p) + (r*((1-b)*p) + r*(b*q)) + (1-r)*(a*q) by
RLVECT_1:def 3
.= (1-r)*((1-a)*p) + r*((1-b)*p) + r*(b*q) + (1-r)*(a*q) by
RLVECT_1:def 3
.= (1-r)*(1-a)*p + r*((1-b)*p) + r*(b*q) + (1-r)*(a*q) by RLVECT_1:def 7
.= (1-r)*(1-a)*p + r*(1-b)*p + r*(b*q) + (1-r)*(a*q) by RLVECT_1:def 7
.= (1-r)*(1-a)*p + r*(1-b)*p + r*b*q + (1-r)*(a*q) by RLVECT_1:def 7
.= (1-r)*(1-a)*p + r*(1-b)*p + r*b*q + (1-r)*a*q by RLVECT_1:def 7
.= ((1-r)*(1-a) + r*(1-b)) * p + r*b*q + (1-r)*a*q by RLVECT_1:def 6
.= ((1-r)*(1-a) + r*(1-b)) * p + (r*b*q + (1-r)*a*q) by RLVECT_1:def 3
.= (1-o)*p + o*q by RLVECT_1:def 6;
hence thesis by A2,A4,A5,A8;
end;
end;
reserve p, q, x for Point of TOP-REAL n;
theorem Th31:
y in Sphere(x,r) & z in Ball(x,r) implies LSeg(y,z) /\ Sphere(x, r) = {y}
proof
set s = y, t = z;
assume that
A1: s in Sphere(x,r) and
A2: t in Ball(x,r);
hereby
let m be object;
assume
A3: m in LSeg(s,t) /\ Sphere(x,r);
then reconsider w = m as Point of TOP-REAL n;
w in LSeg(s,t) by A3,XBOOLE_0:def 4;
then consider d being Real such that
A4: 0 <= d and
A5: d <= 1 and
A6: w = (1-d)*s + d*t by RLTOPSP1:76;
A7: |. d*(t-x) .| = |.d.|*|. t-x .| by TOPRNS_1:7
.= d*|. t-x .| by A4,ABSVALUE:def 1;
d-1 <= 1-1 by A5,XREAL_1:9;
then
A8: -(0 qua Element of NAT) <= -(d-1);
A9: |. (1-d)*(s-x) .| = |.1-d.|*|. s-x .| by TOPRNS_1:7
.= (1-d)*|. s-x .| by A8,ABSVALUE:def 1
.= (1-d)*r by A1,Th7;
m in Sphere(x,r) by A3,XBOOLE_0:def 4;
then
A10: r = |. w - x .| by Th7
.= |. (1-d)*s + d*t - (1-d+d)*x .| by A6,RLVECT_1:def 8
.= |. (1-d)*s + d*t - ((1-d)*x + d*x) .| by RLVECT_1:def 6
.= |. (1-d)*s + d*t - (1-d)*x - d*x .| by RLVECT_1:27
.= |. (1-d)*s - (1-d)*x + d*t - d*x .| by RLVECT_1:def 3
.= |. (1-d)*(s-x) + d*t - d*x .| by RLVECT_1:34
.= |. (1-d)*(s-x) + (d*t - d*x) .| by RLVECT_1:def 3
.= |. (1-d)*(s-x) + d*(t-x) .| by RLVECT_1:34;
per cases by A4;
suppose
A11: d > 0;
|. t-x .| < r by A2,Th5;
then d*|. t-x .| < d*r by A11,XREAL_1:68;
then (1-d)*r + d*|. t-x .| < (1-d)*r + d*r by XREAL_1:8;
hence m in {s} by A10,A9,A7,TOPRNS_1:29;
end;
suppose
d = 0;
then m = 1 * s + 0.TOP-REAL n by A6,RLVECT_1:10
.= 1 * s by RLVECT_1:4
.= s by RLVECT_1:def 8;
hence m in {s} by TARSKI:def 1;
end;
end;
let m be object;
A12: s in LSeg(s,t) by RLTOPSP1:68;
assume m in {s};
then m = s by TARSKI:def 1;
hence thesis by A1,A12,XBOOLE_0:def 4;
end;
theorem Th32:
y in Sphere(x,r) & z in Sphere(x,r) implies LSeg(y,z) \ {y,z} c= Ball(x,r)
proof
assume that
A1: y in Sphere(x,r) and
A2: z in Sphere(x,r);
per cases;
suppose
y = z;
then LSeg(y,z) = {y} & {y,z} = {y} by ENUMSET1:29,RLTOPSP1:70;
then LSeg(y,z) \ {y,z} = {} by XBOOLE_1:37;
hence thesis;
end;
suppose
A3: y <> z;
the carrier of TOP-REAL n = REAL n by EUCLID:22
.= n-tuples_on REAL;
then reconsider xf = x, yf = y, zf = z as Element of n-tuples_on REAL;
reconsider yyf = yf, zzf = zf, xxf = xf as Element of REAL n;
reconsider y1 = y-x, z1 = z-x as FinSequence of REAL;
set X = |(y-x,z-x)|;
let a be object;
A4: Sum sqr (zf-xf) = |.z1.|^2 by Th3;
A5: |. z-x .|^2 = r^2 by A2,Th7;
assume
A6: a in LSeg(y,z) \ {y,z};
then reconsider R = a as Point of TOP-REAL n;
A7: R in LSeg(y,z) by A6,XBOOLE_0:def 5;
then consider l being Real such that
A8: 0 <= l and
A9: l <= 1 and
A10: R = (1-l)*y + l*z by RLTOPSP1:76;
set l1 = 1-l;
reconsider W1 = l1*(y-x), W2 = l*(z-x) as Element of REAL n by EUCLID:22;
A11: Sum sqr (yf-zf) >= 0 by RVSUM_1:86;
reconsider Rf=R-x as FinSequence of REAL;
A12: W1 + W2 = l1*y-l1*x+l*(z-x) by RLVECT_1:34
.= l1*y-l1*x+(l*z-l*x) by RLVECT_1:34
.= l1*y-l1*x+l*z-l*x by RLVECT_1:def 3
.= l1*y+l*z-l1*x-l*x by RLVECT_1:def 3
.= l1*y+l*z-(l1*x+l*x) by RLVECT_1:27
.= l1*y+l*z-(1 *x-l*x+l*x) by RLVECT_1:35
.= l1*y+l*z-1 *x by RLVECT_4:1
.= Rf by A10,RLVECT_1:def 8;
reconsider W1, W2 as Element of n-tuples_on REAL;
A13: mlt(W1,W2) = (l1*mlt(yf-xf,l*(zf-xf))) by RVSUM_1:65;
A14: sqr W1 = (l1^2*sqr (yf-xf)) by RVSUM_1:58;
Sum sqr Rf >= 0 by RVSUM_1:86;
then |. R-x .|^2 = Sum sqr Rf by SQUARE_1:def 2
.= Sum (sqr W1 + 2*mlt(W1,W2) + sqr W2) by A12,RVSUM_1:68
.= Sum (sqr W1 + 2*mlt(W1,W2)) + Sum sqr W2 by RVSUM_1:89
.= Sum sqr W1 + Sum (2*mlt(W1,W2)) + Sum sqr W2 by RVSUM_1:89
.= l1^2*Sum sqr (yf-xf) + Sum (2*mlt(W1,W2)) + Sum sqr (l*(zf-xf)) by A14
,RVSUM_1:87
.= l1^2*Sum sqr (yf-xf) + Sum (2*mlt(W1,W2)) + Sum (l^2*sqr (zf-xf))
by RVSUM_1:58
.= l1^2*Sum sqr (yf-xf) + Sum (2*mlt(W1,W2)) + l^2*Sum sqr (zf-xf) by
RVSUM_1:87
.= l1^2*|.y1.|^2 + Sum (2*mlt(W1,W2)) + l^2*Sum sqr (zf-xf) by Th3
.= l1^2*r^2 + Sum (2*mlt(W1,W2)) + l^2*|.z1.|^2 by A1,A4,Th7
.= l1^2*r^2 + 2*Sum mlt(W1,W2) + l^2*r^2 by A5,RVSUM_1:87
.= l1^2*r^2 + 2*Sum (l1*(l*mlt(yf-xf,zf-xf))) + l^2*r^2 by A13,RVSUM_1:65
.= l1^2*r^2 + 2*Sum (l1*l*mlt(yf-xf,zf-xf)) + l^2*r^2 by RVSUM_1:49
.= l1^2*r^2 + 2*(l1*l*Sum mlt(yf-xf,zf-xf)) + l^2*r^2 by RVSUM_1:87
.= l1^2*r^2 + 2*l1*l*Sum mlt(yf-xf,zf-xf) + l^2*r^2
.= l1^2*r^2 + 2*l1*l*X + l^2*r^2 by RVSUM_1:def 16
.= (1-2*l+l^2+l^2)*r^2 + 2*l*l1*X;
then
A15: |. R-x .|^2 - r^2 = 2*l*l1*(-r^2+X);
now
assume l = 0;
then R = y by A10,Th2;
then R in {y,z} by TARSKI:def 2;
hence contradiction by A6,XBOOLE_0:def 5;
end;
then
A16: 2*l > 0 by A8,XREAL_1:129;
A17: now
assume l1 = 0;
then R = z by A10,Th2;
then R in {y,z} by TARSKI:def 2;
hence contradiction by A6,XBOOLE_0:def 5;
end;
1-1 <= l1 by A9,XREAL_1:13;
then
A18: 2*l*l1 > 0 by A16,A17,XREAL_1:129;
A19: |. y-x .|^2 = r^2 by A1,Th7;
A20: now
assume |. R-x .| = r;
then X-r^2 = 0 by A15,A18,XCMPLX_1:6;
then 0 = |. y-x .|^2 - 2*X + |. z-x .|^2 by A2,A19,Th7
.= |. y-x - (z-x) .|^2 by EUCLID_2:46
.= |. y-x-z+x .|^2 by RLVECT_1:29
.= |. y-x+x-z .|^2 by RLVECT_1:def 3
.= |.yf-zf.|^2 by RLVECT_4:1
.= Sum sqr (yf-zf) by A11,SQUARE_1:def 2;
then yf-zf = n |-> 0 by RVSUM_1:91;
hence contradiction by A3,RVSUM_1:38;
end;
Sphere(x,r) c= cl_Ball(x,r) by Th15;
then LSeg(y,z) c= cl_Ball(x,r) by A1,A2,JORDAN1:def 1;
then |. R-x .| <= r by A7,Th6;
then |. R-x .| < r by A20,XXREAL_0:1;
hence thesis;
end;
end;
theorem Th33:
y in Sphere(x,r) & z in Sphere(x,r) implies LSeg(y,z) /\ Sphere( x,r) = {y,z}
proof
A1: y in LSeg(y,z) & z in LSeg(y,z) by RLTOPSP1:68;
assume
A2: y in Sphere(x,r) & z in Sphere(x,r);
then
A3: LSeg(y,z) \ {y,z} c= Ball(x,r) by Th32;
hereby
let a be object;
assume
A4: a in LSeg(y,z) /\ Sphere(x,r);
assume
A5: not a in {y,z};
a in LSeg(y,z) by A4,XBOOLE_0:def 4;
then
A6: a in LSeg(y,z) \ {y,z} by A5,XBOOLE_0:def 5;
A7: Ball(x,r) misses Sphere(x,r) by Th17;
a in Sphere(x,r) by A4,XBOOLE_0:def 4;
hence contradiction by A3,A6,A7,XBOOLE_0:3;
end;
let a be object;
assume a in {y,z};
then a = y or a = z by TARSKI:def 2;
hence thesis by A2,A1,XBOOLE_0:def 4;
end;
theorem Th34:
y in Sphere(x,r) & z in Sphere(x,r) implies halfline(y,z) /\
Sphere(x,r) = {y,z}
proof
assume that
A1: y in Sphere(x,r) and
A2: z in Sphere(x,r);
per cases;
suppose
A3: y = z;
then
A4: {y,z} = {y} by ENUMSET1:29;
A5: halfline(y,z) = {y} by A3,Th27;
hence
for m being object st m in halfline(y,z) /\ Sphere(x,r) holds m in {y,z}
by A4,XBOOLE_0:def 4;
let m be object;
assume
A6: m in {y,z};
then m = y by A4,TARSKI:def 1;
hence thesis by A1,A5,A4,A6,XBOOLE_0:def 4;
end;
suppose
A7: y <> z;
hereby
let m be object;
assume
A8: m in halfline(y,z) /\ Sphere(x,r);
then
A9: m in Sphere(x,r) by XBOOLE_0:def 4;
reconsider w = m as Point of TOP-REAL n by A8;
m in halfline(y,z) by A8,XBOOLE_0:def 4;
then consider R being Real such that
A10: m = (1-R)*y + R*z and
A11: 0 <= R;
reconsider R as Real;
per cases by A11,XXREAL_0:1;
suppose
R = 0;
then m = y by A10,Th2;
hence m in {y,z} by TARSKI:def 2;
end;
suppose
R = 1;
then m = z by A10,Th2;
hence m in {y,z} by TARSKI:def 2;
end;
suppose
A12: R > 0 & R < 1;
A13: now
assume m in {y,z};
then m = y or m = z by TARSKI:def 2;
hence contradiction by A7,A10,A12,Th2;
end;
w in LSeg(y,z) by A10,A12;
then
A14: m in LSeg(y,z) \ {y,z} by A13,XBOOLE_0:def 5;
LSeg(y,z) \ {y,z} c= Ball(x,r) by A1,A2,Th32;
then |. w-x .| < r by A14,Th5;
hence m in {y,z} by A9,Th7;
end;
suppose
A15: R > 1;
then
A16: 1/R < 1 by XREAL_1:212;
A17: (1-1/R)*y + 1/R*w = (1-1/R)*y + (1/R*((1-R)*y) + 1/R*(R*z)) by A10,
RLVECT_1:def 5
.= (1-1/R)*y + (1/R*((1-R)*y) + 1/R*R*z) by RLVECT_1:def 7
.= (1-1/R)*y + (1/R*((1-R)*y) + 1 * z) by A15,XCMPLX_1:87
.= (1-1/R)*y + (1/R*((1-R)*y) + z) by RLVECT_1:def 8
.= (1-1/R)*y + 1/R*((1-R)*y) + z by RLVECT_1:def 3
.= (1-1/R)*y + 1/R*(1-R)*y + z by RLVECT_1:def 7
.= (1-1/R+1/R*(1-R))*y + z by RLVECT_1:def 6
.= (1-1/R+1/R*1-1/R*R)*y + z
.= (1-1/R+1/R*1-1)*y + z by A15,XCMPLX_1:87
.= 0.TOP-REAL n + z by RLVECT_1:10
.= z by RLVECT_1:4;
A18: now
assume z in {y,w};
then z = y or z = w by TARSKI:def 2;
hence contradiction by A7,A16,A17,Th2;
end;
z in LSeg(y,w) by A15,A16,A17;
then
A19: z in LSeg(y,w) \ {y,w} by A18,XBOOLE_0:def 5;
LSeg(y,w) \ {y,w} c= Ball(x,r) by A1,A9,Th32;
then |. z-x .| < r by A19,Th5;
hence m in {y,z} by A2,Th7;
end;
end;
let m be object;
assume m in {y,z};
then
A20: m = y or m = z by TARSKI:def 2;
y in halfline(y,z) & z in halfline(y,z) by Th25,Th26;
hence thesis by A1,A2,A20,XBOOLE_0:def 4;
end;
end;
theorem Th35:
for S, T, X being Element of REAL n st S = y & T = z & X = x
holds y <> z & y in Ball(x,r) & a = (-(2*|(z-y,y-x)|) +
sqrt delta (Sum sqr (T- S), 2 * |(z-y,y-x)|, Sum sqr (S-X) - r^2))
/ (2 * Sum sqr (T-S)) implies ex e
being Point of TOP-REAL n st {e} = halfline(y,z) /\ Sphere(x,r) & e = (1-a)*y +
a*z
proof
let S, T, X be Element of REAL n such that
A1: S = y and
A2: T = z and
A3: X = x;
set s = y, t = z;
A4: Sum sqr (T-S) >= 0 by RVSUM_1:86;
then
A5: |. T-S .|^2 = Sum sqr (T-S) by SQUARE_1:def 2;
set A = Sum sqr (T-S);
assume that
A6: s <> t and
A7: s in Ball(x,r) and
A8: a = (-(2*|(z-y,y-x)|) + sqrt delta (Sum sqr (T-S), 2 * |(z-y,y-x)|,
Sum sqr (S-X) - r^2)) / (2 * Sum sqr (T-S));
A9: |. T-S .| <> 0 by A1,A2,A6,EUCLID:16;
A10: now
assume A <= 0;
then A = 0 by RVSUM_1:86;
hence contradiction by A9;
end;
set C = Sum sqr (S-X) - r^2;
set B = 2 * |(t-s,s-x)|;
A11: r = 0 or r <> 0;
Sum sqr (S-X) >= 0 by RVSUM_1:86;
then
A12: |. S-X .|^2 = Sum sqr (S-X) by SQUARE_1:def 2;
|. s-x .| < r by A7,Th5;
then (sqrt Sum sqr (S-X))^2 < r^2 by A1,A3,SQUARE_1:16;
then
A13: C < 0 by A12,XREAL_1:49;
then
A14: C/A < 0 by A10,XREAL_1:141;
set l2 = (- B + sqrt delta(A,B,C)) / (2 * A);
set l1 = (- B - sqrt delta(A,B,C)) / (2 * A);
take e1 = (1-l2)*s+l2*t;
A15: 0 <= --r by A7;
A16: delta(A,B,C) = B^2 - 4*A*C & B^2 >= 0 by QUIN_1:def 1,XREAL_1:63;
A17: for x being Real holds Polynom(A,B,C,x) = Quard(A,l1,l2,x)
proof
let x be Real;
thus Polynom(A,B,C,x) = A*x^2+B*x+C by POLYEQ_1:def 2
.= A*(x-l1)*(x-l2) by A10,A13,A16,QUIN_1:16
.= A*((x-l1)*(x-l2))
.= Quard(A,l1,l2,x) by POLYEQ_1:def 3;
end;
then C/A = l1*l2 by A10,POLYEQ_1:11;
then
A18: l1 < 0 & l2 > 0 or l1 > 0 & l2 < 0 by A14,XREAL_1:133;
A19: A*l2^2+B*l2--C = Polynom(A,B,C,l2) by POLYEQ_1:def 2
.= Quard(A,l1,l2,l2) by A17
.= A*((l2-l1)*(l2-l2)) by POLYEQ_1:def 3
.= 0;
|. e1 - x .|^2 = |. 1 * s - l2*s + l2*t - x .|^2 by RLVECT_1:35
.= |. s - l2*s + l2*t - x .|^2 by RLVECT_1:def 8
.= |. s + l2*t - l2*s - x .|^2 by RLVECT_1:def 3
.= |. s + (l2*t - l2*s) - x .|^2 by RLVECT_1:def 3
.= |. s - x + (l2*t - l2*s) .|^2 by RLVECT_1:def 3
.= |. s-x + l2*(t-s) .|^2 by RLVECT_1:34
.= |. s-x .|^2 + 2*|(l2*(t-s),s-x)| + |. l2*(t-s) .|^2 by EUCLID_2:45
.= Sum sqr (S-X) + 2*(l2*|(t-s,s-x)|) + |. l2*(t-s) .|^2
by A12,A1,A3,EUCLID_2:19
.= Sum sqr (S-X) + 2*l2*|(t-s,s-x)| + (|.l2.|*|. t-s .|)^2 by TOPRNS_1:7
.= Sum sqr (S-X) + 2*l2*|(t-s,s-x)| + (|.l2.|)^2*|. t-s .|^2
.= Sum sqr (S-X) + l2*(2 * |(t-s,s-x)|) + l2^2*(|. T-S .|^2)
by A1,A2,COMPLEX1:75
.= Sum sqr (S-X) + l2*B + l2^2*A by A4,SQUARE_1:def 2
.= r^2 by A19;
then |. e1 - x .| = r or |. e1 - x .| = -r by SQUARE_1:40;
then
A20: e1 in Sphere(x,r) by A15,A11;
A21: 4*A*C < 0 by A10,A13,XREAL_1:129,132;
then
A22: e1 in halfline(s,t) by A10,A16,A18,QUIN_1:25;
hereby
let d be object;
assume d in {e1};
then d = e1 by TARSKI:def 1;
hence d in halfline(s,t) /\ Sphere(x,r) by A22,A20,XBOOLE_0:def 4;
end;
hereby
let d be object;
assume
A23: d in halfline(s,t) /\ Sphere(x,r);
then d in halfline(s,t) by XBOOLE_0:def 4;
then consider l being Real such that
A24: d = (1-l)*s+l*t and
A25: 0 <= l;
A26: |. l*(t-s) .|^2 = (|.l.|*|. t-s .|)^2 by TOPRNS_1:7
.= |.l.|^2 * |. t-s .|^2
.= l^2 * |. t-s .|^2 by COMPLEX1:75;
d in Sphere(x,r) by A23,XBOOLE_0:def 4;
then r = |. (1-l)*s+l*t - x .| by A24,Th7
.= |. 1 * s - l*s + l*t - x .| by RLVECT_1:35
.= |. s - l*s + l*t - x .| by RLVECT_1:def 8
.= |. s - (l*s - l*t) - x .| by RLVECT_1:29
.= |. s +- (l*s - l*t) +- x .|
.= |. s +-x +- (l*s - l*t) .| by RLVECT_1:def 3
.= |. s-x - (l*s - l*t) .|
.= |. s +-x +-(l*s - l*t) .|
.= |. s-x +- l*(s-t) .| by RLVECT_1:34
.= |. s-x + l*(-(s-t)) .| by RLVECT_1:25
.= |. s-x + l*(t-s) .| by RLVECT_1:33;
then r^2 = |. s-x .|^2 + 2*|(l*(t-s),s-x)| + |. l*(t-s) .|^2 by EUCLID_2:45
.= |. s-x .|^2 + 2*(l*|(t-s,s-x)|) + |. l*(t-s) .|^2 by EUCLID_2:19;
then A*l^2+B*l+C = 0 by A5,A12,A1,A3,A2,A26;
then Polynom(A,B,C,l) = 0 by POLYEQ_1:def 2;
then l = l1 or l = l2 by A10,A13,A16,POLYEQ_1:5;
hence d in {e1} by A10,A21,A16,A18,A24,A25,QUIN_1:25,TARSKI:def 1;
end;
thus thesis by A8;
end;
theorem Th36:
for S, T, Y being Element of REAL n st S = 1/2*y + 1/2*z & T = z
& Y = x & y <> z & y in Sphere(x,r) & z in cl_Ball(x,r) ex e being Point of
TOP-REAL n st e <> y & {y,e} = halfline(y,z) /\ Sphere(x,r) & (z in Sphere(x,r)
implies e = z) & (not z in Sphere(x,r) & a = (-(2*|(z-(1/2*y + 1/2*z),1/2*y + 1
/2*z-x)|) + sqrt delta (Sum sqr (T-S), 2 * |(z-(1/2*y + 1/2*z),1/2*y + 1/2*z-x
)|, Sum sqr (S-Y) - r^2)) / (2 * Sum sqr (T-S)) implies e = (1-a)*(1/2*y + 1/2*
z) + a*z)
proof
let S, T, Y be Element of REAL n such that
A1: S = 1/2*y + 1/2*z & T = z & Y = x;
reconsider G = x as Point of Euclid n by TOPREAL3:8;
set s = y, t = z;
set X = 1/2 * s + 1/2 * t;
assume that
A2: s <> t and
A3: s in Sphere(x,r) and
A4: t in cl_Ball(x,r);
A5: Ball(G,r) = Ball(x,r) by Th11;
A6: Sphere(x,r) c= cl_Ball(x,r) by Th15;
per cases;
suppose
A7: t in Sphere(x,r);
take t;
thus thesis by A2,A3,A7,Th34;
end;
suppose
A8: not t in Sphere(x,r);
A9: now
assume
A10: X = t;
t +- 1/2 * s +- 1/2 * t = t - 1/2 * s - 1/2 * t
.= t - t by A10,RLVECT_1:27
.= 0.TOP-REAL n by RLVECT_1:5;
then 0.TOP-REAL n
= t +- 1/2 * t +- 1/2 * s by RLVECT_1:def 3
.= 1 * t - 1/2 * t - 1/2 * s by RLVECT_1:def 8
.= (1-1/2) * t - 1/2 * s by RLVECT_1:35
.= 1/2 * (t-s) by RLVECT_1:34;
then t-s = 0.TOP-REAL n by RLVECT_1:11;
hence contradiction by A2,RLVECT_1:21;
end;
Ball(x,r) \/ Sphere(x,r) = cl_Ball(x,r) by Th16;
then
A11: t in Ball(G,r) by A4,A5,A8,XBOOLE_0:def 3;
set a = (-(2*|(t-X,X-x)|) + sqrt delta (Sum sqr (T-S), 2 * |(t-X,X-x)|,
Sum sqr (S-Y) - r^2)) / (2 * Sum sqr (T-S));
A12: 1/2 + 1/2 = 1 & |.1/2.| = 1/2 by ABSVALUE:def 1;
Ball(G,r) = Ball(x,r) by Th11;
then X in Ball(G,r) by A3,A6,A12,A11,Th22;
then consider e1 being Point of TOP-REAL n such that
A13: {e1} = halfline(X,t) /\ Sphere(x,r) and
A14: e1 = (1-a)*X + a*t by A1,A5,A9,Th35;
take e1;
A15: e1 in {e1} by TARSKI:def 1;
then e1 in halfline(X,t) by A13,XBOOLE_0:def 4;
then consider l being Real such that
A16: e1 = (1-l)*X + l*t and
A17: 0 <= l;
hereby
assume e1 = s;
then 0.TOP-REAL n = (1-l)*X + l*t - s by A16,RLVECT_1:5
.= (1-l)*(1/2*s) + (1-l)*(1/2*t) + l*t - s by RLVECT_1:def 5
.= (1-l)*(1/2*s) + ((1-l)*(1/2*t) + l*t) - s by RLVECT_1:def 3
.= (1-l)*(1/2*s) - s + ((1-l)*(1/2*t) + l*t) by RLVECT_1:def 3
.= (1-l)*(1/2*s) - 1 * s + ((1-l)*(1/2*t) + l*t) by RLVECT_1:def 8
.= (1-l)*(1/2)*s - 1 * s + ((1-l)*(1/2*t) + l*t) by RLVECT_1:def 7
.= ((1-l)*(1/2) - 1) * s + ((1-l)*(1/2*t) + l*t) by RLVECT_1:35
.= (-1/2 - l*(1/2)) * s + ((1-l)*(1/2)*t + l*t) by RLVECT_1:def 7
.= (-1/2 - l*(1/2)) * s + ((1-l)*(1/2) + l) * t by RLVECT_1:def 6
.= (-(1/2 + l*(1/2))) * s + (1/2 + l*(1/2)) * t
.= (1/2 + l*(1/2)) * t - (1/2 + l*(1/2)) * s by RLVECT_1:79
.= (1/2 + l*(1/2)) * (t - s) by RLVECT_1:34;
then 1/2 + l*(1/2) = 0 or t - s = 0.TOP-REAL n by RLVECT_1:11;
hence contradiction by A2,A17,RLVECT_1:21;
end;
A18: s in halfline(s,t) by Th25;
hereby
set o = (1+l)/2;
let m be object;
assume m in {s,e1};
then
A19: m = s or m = e1 by TARSKI:def 2;
e1 = (1-l)*(1/2*s) + (1-l)*(1/2*t) + l*t by A16,RLVECT_1:def 5
.= (1-l)*(1/2)*s + (1-l)*(1/2*t) + l*t by RLVECT_1:def 7
.= (1-l)*(1/2)*s + (1-l)*(1/2)*t + l*t by RLVECT_1:def 7
.= (1-l)*(1/2)*s + ((1-l)*(1/2)*t + l*t) by RLVECT_1:def 3
.= (1-l)*(1/2)*s + ((1-l)*(1/2) + l)*t by RLVECT_1:def 6
.= (1-o)*s + o*t;
then
A20: e1 in halfline(s,t) by A17;
e1 in Sphere(x,r) by A13,A15,XBOOLE_0:def 4;
hence m in halfline(s,t) /\ Sphere(x,r) by A3,A18,A19,A20,XBOOLE_0:def 4;
end;
hereby
let m be object;
assume
A21: m in halfline(s,t) /\ Sphere(x,r);
then
A22: m in halfline(s,t) by XBOOLE_0:def 4;
A23: m in Sphere(x,r) by A21,XBOOLE_0:def 4;
per cases;
suppose
m in halfline(X,t);
then m in halfline(X,t) /\ Sphere(x,r) by A23,XBOOLE_0:def 4;
then m = e1 by A13,TARSKI:def 1;
hence m in {s,e1} by TARSKI:def 2;
end;
suppose
A24: not m in halfline(X,t);
consider M being Real such that
A25: m = (1-M)*s + M*t and
A26: 0 <= M by A22;
A27: now
set o = 2*M-1;
assume M > 1;
then 2*M > 2*1 by XREAL_1:68;
then
A28: 2*M-1 > 2*1-1 by XREAL_1:14;
(1-o)*X + o*t = (1-o)*(1/2 * s) + (1-o)*(1/2 * t) + o*t by
RLVECT_1:def 5
.= (1-o)*(1/2) * s + (1-o)*(1/2 * t) + o*t by RLVECT_1:def 7
.= (1-o)*(1/2) * s + (1-o)*(1/2) * t + o*t by RLVECT_1:def 7
.= (1-o)*(1/2) * s + ((1-o)*(1/2) * t + o*t) by RLVECT_1:def 3
.= (1-o)*(1/2) * s + ((1-o)*(1/2)+o) * t by RLVECT_1:def 6
.= m by A25;
hence contradiction by A24,A28;
end;
|. t-x .| <= r & |. t-x .| <> r by A4,A8,Th6;
then |. t-x .| < r by XXREAL_0:1;
then t in Ball(x,r);
then
A29: LSeg(s,t) /\ Sphere(x,r) = {s} by A3,Th31;
m in LSeg(s,t) by A25,A26,A27;
then m in {s} by A23,A29,XBOOLE_0:def 4;
then m = s by TARSKI:def 1;
hence m in {s,e1} by TARSKI:def 2;
end;
end;
thus thesis by A8,A14;
end;
end;
registration
let n be Nat, x be Point of TOP-REAL n;
let r be negative Real;
cluster Sphere(x,r) -> empty;
coherence
proof
assume not thesis;
then consider y being Point of TOP-REAL n such that
A1: y in Sphere(x,r);
|. y - x .| = r by A1,Th7;
hence contradiction;
end;
end;
registration
let n be non zero Nat, x be Point of TOP-REAL n;
let r be non negative Real;
cluster Sphere(x,r) -> non empty;
coherence
proof
reconsider e = x as Point of Euclid n by TOPREAL3:8;
per cases;
suppose
r = 0;
then Sphere(e,r) = {e} by TOPREAL6:54;
hence thesis by Th13;
end;
suppose
r > 0;
then reconsider r as positive Real;
consider s being Point of TOP-REAL n such that
A1: s in Ball(x,r) by SUBSET_1:4;
reconsider S = s, T = s + 1.REAL n, XX = x as Element of REAL n by
EUCLID:22;
set a = (-(2*|(s + 1.REAL n-s,s-x)|) + sqrt delta (Sum sqr (T-S), 2 * |(
s + 1.REAL n-s,s-x)|, Sum sqr (S-XX) - r^2)) / (2 * Sum sqr (T-S));
s <> s + 1.REAL n by Th1;
then
ex e being Point of TOP-REAL n st {e} = halfline(s,s + 1.REAL n) /\
Sphere(x,r) & e = (1-a)*s + a*(s+1.REAL n) by A1,Th35;
hence thesis;
end;
end;
end;
theorem
Sphere(x,r) is non empty implies r >= 0;
theorem
n is non zero & Sphere(x,r) is empty implies r < 0;
begin :: Subsets of TOP-REAL 2
reserve s, t for Point of TOP-REAL 2;
theorem
(a*s + b*t)`1 = a * s`1 + b * t`1
proof
thus (a*s+b*t)`1 = (a*s)`1 + (b*t)`1 by TOPREAL3:2
.= a*s`1 + (b*t)`1 by TOPREAL3:4
.= a*s`1+b*t`1 by TOPREAL3:4;
end;
theorem
(a*s + b*t)`2 = a * s`2 + b * t`2
proof
thus (a*s+b*t)`2 = (a*s)`2 + (b*t)`2 by TOPREAL3:2
.= a*s`2 + (b*t)`2 by TOPREAL3:4
.= a*s`2+b*t`2 by TOPREAL3:4;
end;
theorem Th41:
t in circle(a,b,r) iff |. t - |[a,b]| .| = r
proof
A1: circle(a,b,r) = {x where x is Point of TOP-REAL 2: |. x - |[a,b]| .| = r
} by JGRAPH_6:def 5;
hereby
assume t in circle(a,b,r);
then
ex x being Point of TOP-REAL 2 st t = x & |. x - |[a,b]| .| = r by A1;
hence |. t - |[a,b]| .| = r;
end;
thus thesis by A1;
end;
theorem Th42:
t in closed_inside_of_circle(a,b,r) iff |. t - |[a,b]| .| <= r
proof
A1: closed_inside_of_circle(a,b,r) = {x where x is Point of TOP-REAL 2: |. x
- |[a,b]| .| <= r} by JGRAPH_6:def 7;
hereby
assume t in closed_inside_of_circle(a,b,r);
then
ex x being Point of TOP-REAL 2 st t = x & |. x - |[a,b]| .| <= r by A1;
hence |. t - |[a,b]| .| <= r;
end;
thus thesis by A1;
end;
theorem Th43:
t in inside_of_circle(a,b,r) iff |. t - |[a,b]| .| < r
proof
A1: inside_of_circle(a,b,r) = {x where x is Point of TOP-REAL 2: |. x - |[a,
b]| .| < r} by JGRAPH_6:def 6;
hereby
assume t in inside_of_circle(a,b,r);
then
ex x being Point of TOP-REAL 2 st t = x & |. x - |[a,b]| .| < r by A1;
hence |. t - |[a,b]| .| < r;
end;
thus thesis by A1;
end;
registration
let a, b be Real;
let r be positive Real;
cluster inside_of_circle(a,b,r) -> non empty;
coherence
proof
|. |[a,b]| - |[a,b]| .| = 0 by TOPRNS_1:28;
hence thesis by Th43;
end;
end;
registration
let a, b be Real;
let r be non negative Real;
cluster closed_inside_of_circle(a,b,r) -> non empty;
coherence
proof
|. |[a,b]| - |[a,b]| .| = 0 by TOPRNS_1:28;
hence thesis by Th42;
end;
end;
theorem
circle(a,b,r) c= closed_inside_of_circle(a,b,r)
proof
let x be object;
assume
A1: x in circle(a,b,r);
then reconsider x as Point of TOP-REAL 2;
|. x - |[a,b]| .| = r by A1,Th41;
hence thesis by Th42;
end;
theorem Th45:
for x being Point of Euclid 2 st x = |[a,b]| holds cl_Ball(x,r)
= closed_inside_of_circle(a,b,r)
proof
let x be Point of Euclid 2 such that
A1: x = |[a,b]|;
hereby
let w be object;
assume
A2: w in cl_Ball(x,r);
then reconsider u = w as Point of TOP-REAL 2 by TOPREAL3:8;
reconsider e = u as Point of Euclid 2 by TOPREAL3:8;
dist(e,x) = |. u - |[a,b]| .| by A1,JGRAPH_1:28;
then |. u - |[a,b]| .| <= r by A2,METRIC_1:12;
hence w in closed_inside_of_circle(a,b,r) by Th42;
end;
let w be object;
assume
A3: w in closed_inside_of_circle(a,b,r);
then reconsider u = w as Point of TOP-REAL 2;
reconsider e = u as Point of Euclid 2 by TOPREAL3:8;
dist(e,x) = |. u - |[a,b]| .| by A1,JGRAPH_1:28;
then dist(e,x) <= r by A3,Th42;
hence thesis by METRIC_1:12;
end;
theorem Th46:
for x being Point of Euclid 2 st x = |[a,b]| holds Ball(x,r) =
inside_of_circle(a,b,r)
proof
let x be Point of Euclid 2 such that
A1: x = |[a,b]|;
hereby
let w be object;
assume
A2: w in Ball(x,r);
then reconsider u = w as Point of TOP-REAL 2 by TOPREAL3:8;
reconsider e = u as Point of Euclid 2 by TOPREAL3:8;
dist(e,x) = |. u - |[a,b]| .| by A1,JGRAPH_1:28;
then |. u - |[a,b]| .| < r by A2,METRIC_1:11;
hence w in inside_of_circle(a,b,r) by Th43;
end;
let w be object;
assume
A3: w in inside_of_circle(a,b,r);
then reconsider u = w as Point of TOP-REAL 2;
reconsider e = u as Point of Euclid 2 by TOPREAL3:8;
dist(e,x) = |. u - |[a,b]| .| by A1,JGRAPH_1:28;
then dist(e,x) < r by A3,Th43;
hence thesis by METRIC_1:11;
end;
theorem Th47:
for x being Point of Euclid 2 st x = |[a,b]| holds Sphere(x,r) =
circle(a,b,r)
proof
let x be Point of Euclid 2 such that
A1: x = |[a,b]|;
hereby
let w be object;
assume
A2: w in Sphere(x,r);
then reconsider u = w as Point of TOP-REAL 2 by TOPREAL3:8;
reconsider e = u as Point of Euclid 2 by TOPREAL3:8;
dist(e,x) = |. u - |[a,b]| .| by A1,JGRAPH_1:28;
then |. u - |[a,b]| .| = r by A2,METRIC_1:13;
hence w in circle(a,b,r) by Th41;
end;
let w be object;
assume
A3: w in circle(a,b,r);
then reconsider u = w as Point of TOP-REAL 2;
reconsider e = u as Point of Euclid 2 by TOPREAL3:8;
dist(e,x) = |. u - |[a,b]| .| by A1,JGRAPH_1:28;
then dist(e,x) = r by A3,Th41;
hence thesis by METRIC_1:13;
end;
theorem Th48:
Ball(|[a,b]|,r) = inside_of_circle(a,b,r)
proof
reconsider e = |[a,b]| as Point of Euclid 2 by TOPREAL3:8;
thus Ball(|[a,b]|,r) = Ball(e,r) by Th11
.= inside_of_circle(a,b,r) by Th46;
end;
theorem
cl_Ball(|[a,b]|,r) = closed_inside_of_circle(a,b,r)
proof
reconsider e = |[a,b]| as Point of Euclid 2 by TOPREAL3:8;
thus cl_Ball(|[a,b]|,r) = cl_Ball(e,r) by Th12
.= closed_inside_of_circle(a,b,r) by Th45;
end;
theorem Th50:
Sphere(|[a,b]|,r) = circle(a,b,r)
proof
reconsider e = |[a,b]| as Point of Euclid 2 by TOPREAL3:8;
thus Sphere(|[a,b]|,r) = Sphere(e,r) by Th13
.= circle(a,b,r) by Th47;
end;
theorem
inside_of_circle(a,b,r) c= closed_inside_of_circle(a,b,r)
proof
let x be object;
assume
A1: x in inside_of_circle(a,b,r);
then reconsider x as Point of TOP-REAL 2;
|. x - |[a,b]| .| < r by A1,Th43;
hence thesis by Th42;
end;
theorem
inside_of_circle(a,b,r) misses circle(a,b,r)
proof
assume not thesis;
then consider x being object such that
A1: x in inside_of_circle(a,b,r) and
A2: x in circle(a,b,r) by XBOOLE_0:3;
reconsider x as Point of TOP-REAL 2 by A1;
|. x - |[a,b]| .| = r by A2,Th41;
hence thesis by A1,Th43;
end;
theorem
inside_of_circle(a,b,r) \/ circle(a,b,r) = closed_inside_of_circle(a,b ,r)
proof
reconsider p = |[a,b]| as Point of Euclid 2 by TOPREAL3:8;
A1: cl_Ball(p,r) = closed_inside_of_circle(a,b,r) by Th45;
Sphere(p,r) = circle(a,b,r) & Ball(p,r) = inside_of_circle(a,b,r) by Th46
,Th47;
hence thesis by A1,METRIC_1:16;
end;
theorem
s in Sphere(0.TOP-REAL 2,r) implies s`1^2 + s`2^2 = r^2
proof
assume s in Sphere(0.TOP-REAL 2,r);
then |. s-0.TOP-REAL 2 .| = r by Th7;
then |. s .| = r by RLVECT_1:13;
hence thesis by JGRAPH_1:29;
end;
theorem
s <> t & s in closed_inside_of_circle(a,b,r) & t in
closed_inside_of_circle(a,b,r) implies r > 0
proof
reconsider x = |[a,b]| as Point of Euclid 2 by TOPREAL3:8;
cl_Ball(x,r) = closed_inside_of_circle(a,b,r) by Th45;
hence thesis by Th4;
end;
theorem
for S, T, X being Element of REAL 2 st S = s & T = t & X = |[a,b]| & w
= (-(2*|(t-s,s-|[a,b]|)|) + sqrt delta (Sum sqr (T-S), 2 * |(t-s,s-|[a,b]|)|,
Sum sqr (S-X) - r^2)) / (2 * Sum sqr (T-S)) & s <> t & s in inside_of_circle(a,
b,r) ex e being Point of TOP-REAL 2 st {e} = halfline(s,t) /\ circle(a,b,r) & e
= (1-w)*s + w*t
proof
A1: Ball(|[a,b]|,r) = inside_of_circle(a,b,r) & Sphere(|[a,b]|,r) = circle(a
,b,r ) by Th48,Th50;
let S, T, X be Element of REAL 2;
assume S = s & T = t & X = |[a,b]| & w = (-(2*|(t-s,s-|[a,b]|)|) + sqrt
delta ( Sum sqr (T-S), 2 * |(t-s,s-|[a,b]|)|, Sum sqr (S-X) - r^2)) / (2 * Sum
sqr (T-S )) & s <> t & s in inside_of_circle(a,b,r);
hence thesis by A1,Th35;
end;
theorem
s in circle(a,b,r) & t in inside_of_circle(a,b,r) implies LSeg(s,t) /\
circle(a,b,r) = {s}
proof
assume
A1: s in circle(a,b,r) & t in inside_of_circle(a,b,r);
reconsider e = |[a,b]| as Point of Euclid 2 by TOPREAL3:8;
A2: inside_of_circle(a,b,r) = Ball(e,r) by Th46
.= Ball(|[a,b]|,r) by Th11;
circle(a,b,r) = Sphere(e,r) by Th47
.= Sphere(|[a,b]|,r) by Th13;
hence thesis by A1,A2,Th31;
end;
theorem
s in circle(a,b,r) & t in circle(a,b,r) implies LSeg(s,t) \ {s,t} c=
inside_of_circle(a,b,r)
proof
assume
A1: s in circle(a,b,r) & t in circle(a,b,r);
reconsider G = |[a,b]| as Point of Euclid 2 by TOPREAL3:8;
Sphere(G,r) = circle(a,b,r) by Th47;
then
A2: Sphere(|[a,b]|,r) = circle(a,b,r) by Th13;
Ball(|[a,b]|,r) = inside_of_circle(a,b,r) by Th48;
hence thesis by A1,A2,Th32;
end;
theorem
s in circle(a,b,r) & t in circle(a,b,r) implies LSeg(s,t) /\ circle(a,
b,r) = {s,t}
proof
reconsider G = |[a,b]| as Point of Euclid 2 by TOPREAL3:8;
Sphere(G,r) = circle(a,b,r) by Th47;
then
A1: Sphere(|[a,b]|,r) = circle(a,b,r) by Th13;
assume s in circle(a,b,r) & t in circle(a,b,r);
hence thesis by A1,Th33;
end;
theorem
s in circle(a,b,r) & t in circle(a,b,r) implies halfline(s,t) /\
circle(a,b,r) = {s,t}
proof
assume
A1: s in circle(a,b,r) & t in circle(a,b,r);
reconsider e = |[a,b]| as Point of Euclid 2 by TOPREAL3:8;
circle(a,b,r) = Sphere(e,r) by Th47
.= Sphere(|[a,b]|,r) by Th13;
hence thesis by A1,Th34;
end;
theorem
for S, T, Y being Element of REAL 2 st S = 1/2*s + 1/2*t & T = t & Y =
|[a,b]| & s <> t & s in circle(a,b,r) & t in closed_inside_of_circle(a,b,r) ex
e being Point of TOP-REAL 2 st e <> s & {s,e} = halfline(s,t) /\ circle(a,b,r)
& (t in Sphere(|[a,b]|,r) implies e = t) & (not t in Sphere(|[a,b]|,r) & w = (-
(2*|(t-(1/2*s + 1/2*t),1/2*s + 1/2*t-|[a,b]|)|) + sqrt delta (Sum sqr (T-S), 2
* |(t-(1/2*s + 1/2*t),1/2*s + 1/2*t-|[a,b]|)|, Sum sqr (S-Y) - r^2)) / (2 * Sum
sqr (T-S)) implies e = (1-w)*(1/2*s + 1/2*t) + w*t)
proof
reconsider G = |[a,b]| as Point of Euclid 2 by TOPREAL3:8;
A1: cl_Ball(G,r) = closed_inside_of_circle(a,b,r) & cl_Ball(G,r) = cl_Ball(
|[a,b ]|,r) by Th12,Th45;
Sphere(G,r) = circle(a,b,r) by Th47;
then
A2: Sphere(|[a,b]|,r) = circle(a,b,r) by Th13;
let S, T, Y be Element of REAL 2;
assume S = 1/2*s + 1/2*t & T = t & Y = |[a,b]| & s <> t & s in circle(a,b,r
) & t in closed_inside_of_circle(a,b,r);
hence thesis by A1,A2,Th36;
end;
registration
let a, b, r be Real;
cluster inside_of_circle(a,b,r) -> convex;
coherence
proof
inside_of_circle(a,b,r) = {q where q is Point of TOP-REAL 2: |.q - |[a
,b]|.| < r } by JGRAPH_6:def 6;
hence thesis by Lm2;
end;
cluster closed_inside_of_circle(a,b,r) -> convex;
coherence
proof
closed_inside_of_circle(a,b,r) = {q where q is Point of TOP-REAL 2: |.
q - |[a,b]|.| <= r } by JGRAPH_6:def 7;
hence thesis by Lm1;
end;
end;
:: 12.11.18 A.T.
theorem Th62:
for V being RealLinearSpace, p1,p2 being Point of V
holds halfline(p1,p2) c= Line(p1,p2)
proof
let V be RealLinearSpace, p1,p2 be Point of V;
let e be object;
assume e in halfline(p1,p2);
then ex r st e =(1-r)*p1 + r*p2 & 0 <= r;
hence e in Line(p1,p2);
end;
theorem Th63:
for V being RealLinearSpace, p1,p2 being Point of V
holds Line(p1,p2) = halfline(p1,p2) \/ halfline(p2,p1)
proof
let V be RealLinearSpace, p1,p2 be Point of V;
thus Line(p1,p2) c= halfline(p1,p2) \/ halfline(p2,p1)
proof let e be object;
assume e in Line(p1,p2);
then consider r such that
A1: e = (1-r)*p1 + r*p2;
now per cases;
case r >= 0;
hence e in halfline(p1,p2) by A1;
end;
case r <= 0;
then
A2: 1-r >= 0;
e = (1-(1-r))*p2 + (1-r)*p1 by A1;
hence e in halfline(p2,p1) by A2;
end;
end;
hence thesis by XBOOLE_0:def 3;
end;
halfline(p1,p2) c= Line(p1,p2) & halfline(p2,p1) c= Line(p1,p2) by Th62;
hence thesis by XBOOLE_1:8;
end;
theorem Th64:
for V being RealLinearSpace, p1,p2,p3 being Point of V
st p1 in halfline(p2,p3)
holds p1 in LSeg(p2,p3) or p3 in LSeg(p2,p1)
proof let V be RealLinearSpace, p1,p2,p3 be Point of V;
assume p1 in halfline(p2,p3);
then consider r such that
A1: p1 = (1-r)*p2 + r*p3 and
A2: 0 <= r;
set s = 1/r;
now per cases;
case r <= 1;
hence p1 in LSeg(p2,p3) by A1,A2;
end;
case
A3: r >= 1;
per cases by A2;
case r = 0;
then p1 = p2 by A1,Th2;
hence p1 in LSeg(p2,p3) by RLTOPSP1:68;
end;
case
A4: r > 0;
then
A5: s*r = 1 by XCMPLX_1:87;
A6: s <= 1 by A3,XREAL_1:183;
A7: r*p3 = p1 - (1-r)*p2 by RLVECT_4:1,A1;
(s*r)*p3 = s*(r*p3) by RLVECT_1:def 7
.= s*p1 - s*((1-r)*p2) by RLVECT_1:34,A7
.= s*p1 - s*(1-r)*p2 by RLVECT_1:def 7;
then p3 = s*p1 - s*(1-r)*p2 by RLVECT_1:def 8,A5
.= s*p1 + (-s*(1-r))*p2 by RLVECT_1:79
.= s*p1 + (1-s)*p2 by A5;
hence p3 in LSeg(p2,p1) by A4,A6;
end;
end;
end;
hence thesis;
end;
theorem
for V being RealLinearSpace, p1,p2,p3 being Point of V holds
p1,p2,p3 are_collinear iff
p1 in LSeg(p2,p3) or p2 in LSeg(p3, p1) or p3 in LSeg(p1,p2)
proof let V be RealLinearSpace, p1,p2,p3 be Point of V;
thus p1,p2,p3 are_collinear implies
p1 in LSeg(p2,p3) or p2 in LSeg(p3, p1) or p3 in LSeg(p1,p2)
proof assume p1,p2,p3 are_collinear;
then consider L being line of V such that
A1: p1 in L and
A2: p2 in L and
A3: p3 in L;
consider x1,x2 being Point of V such that
A4: L = Line(x1,x2) by RLTOPSP1:def 15;
per cases;
suppose p2 = p3;
hence thesis by RLTOPSP1:68;
end;
suppose p2 <> p3;
then
A5: Line(p2,p3) = L by A2,A3,RLTOPSP1:75,A4;
per cases;
suppose p1 in halfline(p2,p3);
hence thesis by Th64;
end;
suppose
A6: not p1 in halfline(p2,p3);
L = halfline(p2,p3) \/ halfline(p3,p2) by Th63,A5;
then p1 in halfline(p3,p2) by A1,XBOOLE_0:def 3,A6;
hence thesis by Th64;
end;
end;
end;
assume p1 in LSeg(p2,p3) or p2 in LSeg(p3, p1) or p3 in LSeg(p1,p2);
then per cases;
suppose
A7: p1 in LSeg(p2,p3);
take Line(p2,p3);
LSeg(p2,p3) c= Line(p2,p3) by RLTOPSP1:73;
hence p1 in Line(p2,p3) by A7;
thus p2 in Line(p2,p3) by RLTOPSP1:72;
thus p3 in Line(p2,p3) by RLTOPSP1:72;
end;
suppose
A8: p2 in LSeg(p3, p1);
take Line(p3,p1);
thus p1 in Line(p3,p1) by RLTOPSP1:72;
LSeg(p3,p1) c= Line(p3,p1) by RLTOPSP1:73;
hence p2 in Line(p3,p1) by A8;
thus p3 in Line(p3,p1) by RLTOPSP1:72;
end;
suppose
A9: p3 in LSeg(p1,p2);
take Line(p1,p2);
thus p1 in Line(p1,p2) by RLTOPSP1:72;
thus p2 in Line(p1,p2) by RLTOPSP1:72;
LSeg(p1,p2) c= Line(p1,p2) by RLTOPSP1:73;
hence p3 in Line(p1,p2) by A9;
end;
end;