:: Intersections of Intervals and Balls in TOP-REAL n :: by Artur Korni{\l}owicz and Yasunari Shidama :: :: Received May 10, 2004 :: Copyright (c) 2004-2021 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; 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 :: TOPREAL9:3 n is non zero implies x <> x + 1.REAL n; theorem :: TOPREAL9:4 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); theorem :: TOPREAL9:5 for f being real-valued FinSequence holds |.f.|^2 = Sum sqr f; theorem :: TOPREAL9:6 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; 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 :: TOPREAL9:def 1 {p where p is Point of TOP-REAL n: |. p-x .| < r}; func cl_Ball(x,r) -> Subset of TOP-REAL n equals :: TOPREAL9:def 2 {p where p is Point of TOP-REAL n: |. p-x .| <= r}; func Sphere(x,r) -> Subset of TOP-REAL n equals :: TOPREAL9:def 3 {p where p is Point of TOP-REAL n: |. p-x .| = r}; end; theorem :: TOPREAL9:7 y in Ball(x,r) iff |. y-x .| < r; theorem :: TOPREAL9:8 y in cl_Ball(x,r) iff |. y-x .| <= r; theorem :: TOPREAL9:9 y in Sphere(x,r) iff |. y-x .| = r; theorem :: TOPREAL9:10 y in Ball(0.TOP-REAL n,r) implies |.y.| < r; theorem :: TOPREAL9:11 y in cl_Ball(0.TOP-REAL n,r) implies |.y.| <= r; theorem :: TOPREAL9:12 y in Sphere(0.TOP-REAL n,r) implies |.y.| = r; theorem :: TOPREAL9:13 x = e implies Ball(e,r) = Ball(x,r); theorem :: TOPREAL9:14 x = e implies cl_Ball(e,r) = cl_Ball(x,r); theorem :: TOPREAL9:15 x = e implies Sphere(e,r) = Sphere(x,r); theorem :: TOPREAL9:16 Ball(x,r) c= cl_Ball(x,r); theorem :: TOPREAL9:17 Sphere(x,r) c= cl_Ball(x,r); theorem :: TOPREAL9:18 Ball(x,r) \/ Sphere(x,r) = cl_Ball(x,r); theorem :: TOPREAL9:19 Ball(x,r) misses Sphere(x,r); registration let n be Nat, x be Point of TOP-REAL n; let r be non positive Real; cluster Ball(x,r) -> empty; end; registration let n be Nat, x be Point of TOP-REAL n; let r be positive Real; cluster Ball(x,r) -> non empty; end; theorem :: TOPREAL9:20 Ball(x,r) is non empty implies r > 0; theorem :: TOPREAL9:21 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; 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; end; theorem :: TOPREAL9:22 cl_Ball(x,r) is non empty implies r >= 0; theorem :: TOPREAL9:23 cl_Ball(x,r) is empty implies r < 0; theorem :: TOPREAL9:24 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); registration let n be Nat, x be Point of TOP-REAL n; let r; cluster Ball(x,r) -> open; cluster cl_Ball(x,r) -> closed; cluster Sphere(x,r) -> closed; end; registration let n,x,r; cluster Ball(x,r) -> bounded; cluster cl_Ball(x,r) -> bounded; cluster Sphere(x,r) -> bounded; 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; cluster cl_Ball(x,r) -> convex; end; definition let n be Nat; let f be Function of TOP-REAL n, TOP-REAL n; attr f is homogeneous means :: TOPREAL9:def 4 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; end; registration let n; cluster homogeneous additive continuous for Function of TOP-REAL n, TOP-REAL n; end; registration let a, c be Real; cluster AffineMap(a,0,c,0) -> homogeneous additive; end; theorem :: TOPREAL9:25 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; :: 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 :: TOPREAL9:def 5 { (1-l)*p + l*q where l is Real: 0 <= l }; end; theorem :: TOPREAL9:26 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; end; theorem :: TOPREAL9:27 p in halfline(p,q); theorem :: TOPREAL9:28 q in halfline(p,q); theorem :: TOPREAL9:29 halfline(p,p) = {p}; theorem :: TOPREAL9:30 x in halfline(p,q) implies halfline(p,x) c= halfline(p,q); theorem :: TOPREAL9:31 x in halfline(p,q) & x <> p implies halfline(p,q) = halfline(p,x); theorem :: TOPREAL9:32 LSeg(p,q) c= halfline(p,q); registration let V, p, q; cluster halfline(p,q) -> convex; end; reserve p, q, x for Point of TOP-REAL n; theorem :: TOPREAL9:33 y in Sphere(x,r) & z in Ball(x,r) implies LSeg(y,z) /\ Sphere(x, r) = {y}; theorem :: TOPREAL9:34 y in Sphere(x,r) & z in Sphere(x,r) implies LSeg(y,z) \ {y,z} c= Ball(x,r); theorem :: TOPREAL9:35 y in Sphere(x,r) & z in Sphere(x,r) implies LSeg(y,z) /\ Sphere( x,r) = {y,z} ; theorem :: TOPREAL9:36 y in Sphere(x,r) & z in Sphere(x,r) implies halfline(y,z) /\ Sphere(x,r) = {y,z}; theorem :: TOPREAL9:37 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; theorem :: TOPREAL9:38 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); registration let n be Nat, x be Point of TOP-REAL n; let r be negative Real; cluster Sphere(x,r) -> empty; 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; end; theorem :: TOPREAL9:39 Sphere(x,r) is non empty implies r >= 0; theorem :: TOPREAL9:40 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 :: TOPREAL9:41 (a*s + b*t)`1 = a * s`1 + b * t`1; theorem :: TOPREAL9:42 (a*s + b*t)`2 = a * s`2 + b * t`2; theorem :: TOPREAL9:43 t in circle(a,b,r) iff |. t - |[a,b]| .| = r; theorem :: TOPREAL9:44 t in closed_inside_of_circle(a,b,r) iff |. t - |[a,b]| .| <= r; theorem :: TOPREAL9:45 t in inside_of_circle(a,b,r) iff |. t - |[a,b]| .| < r; registration let a, b be Real; let r be positive Real; cluster inside_of_circle(a,b,r) -> non empty; end; registration let a, b be Real; let r be non negative Real; cluster closed_inside_of_circle(a,b,r) -> non empty; end; theorem :: TOPREAL9:46 circle(a,b,r) c= closed_inside_of_circle(a,b,r); theorem :: TOPREAL9:47 for x being Point of Euclid 2 st x = |[a,b]| holds cl_Ball(x,r) = closed_inside_of_circle(a,b,r); theorem :: TOPREAL9:48 for x being Point of Euclid 2 st x = |[a,b]| holds Ball(x,r) = inside_of_circle(a,b,r); theorem :: TOPREAL9:49 for x being Point of Euclid 2 st x = |[a,b]| holds Sphere(x,r) = circle(a,b,r); theorem :: TOPREAL9:50 Ball(|[a,b]|,r) = inside_of_circle(a,b,r); theorem :: TOPREAL9:51 cl_Ball(|[a,b]|,r) = closed_inside_of_circle(a,b,r); theorem :: TOPREAL9:52 Sphere(|[a,b]|,r) = circle(a,b,r); theorem :: TOPREAL9:53 inside_of_circle(a,b,r) c= closed_inside_of_circle(a,b,r); theorem :: TOPREAL9:54 inside_of_circle(a,b,r) misses circle(a,b,r); theorem :: TOPREAL9:55 inside_of_circle(a,b,r) \/ circle(a,b,r) = closed_inside_of_circle(a,b ,r); theorem :: TOPREAL9:56 s in Sphere(0.TOP-REAL 2,r) implies s`1^2 + s`2^2 = r^2; theorem :: TOPREAL9:57 s <> t & s in closed_inside_of_circle(a,b,r) & t in closed_inside_of_circle(a,b,r) implies r > 0; theorem :: TOPREAL9:58 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; theorem :: TOPREAL9:59 s in circle(a,b,r) & t in inside_of_circle(a,b,r) implies LSeg(s,t) /\ circle(a,b,r) = {s}; theorem :: TOPREAL9:60 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); theorem :: TOPREAL9:61 s in circle(a,b,r) & t in circle(a,b,r) implies LSeg(s,t) /\ circle(a, b,r) = {s,t}; theorem :: TOPREAL9:62 s in circle(a,b,r) & t in circle(a,b,r) implies halfline(s,t) /\ circle(a,b,r) = {s,t}; theorem :: TOPREAL9:63 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); registration let a, b, r be Real; cluster inside_of_circle(a,b,r) -> convex; cluster closed_inside_of_circle(a,b,r) -> convex; end; :: 12.11.18 A.T. theorem :: TOPREAL9:64 for V being RealLinearSpace, p1,p2 being Point of V holds halfline(p1,p2) c= Line(p1,p2); theorem :: TOPREAL9:65 for V being RealLinearSpace, p1,p2 being Point of V holds Line(p1,p2) = halfline(p1,p2) \/ halfline(p2,p1); theorem :: TOPREAL9:66 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); theorem :: TOPREAL9:67 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);