Documentation

Mathlib.Geometry.Euclidean.Sphere.Basic

Spheres #

This file defines and proves basic results about spheres and cospherical sets of points in Euclidean affine spaces.

Main definitions #

theorem EuclideanGeometry.Sphere.ext_iff {P : Type u_2} :
∀ {inst : MetricSpace P} {x y : EuclideanGeometry.Sphere P}, x = y x.center = y.center x.radius = y.radius
theorem EuclideanGeometry.Sphere.ext {P : Type u_2} :
∀ {inst : MetricSpace P} {x y : EuclideanGeometry.Sphere P}, x.center = y.centerx.radius = y.radiusx = y
structure EuclideanGeometry.Sphere (P : Type u_2) [MetricSpace P] :
Type u_2

A Sphere P bundles a center and radius. This definition does not require the radius to be positive; that should be given as a hypothesis to lemmas that require it.

  • center : P

    center of this sphere

  • radius :

    radius of the sphere: not required to be positive

Instances For
    Equations
    Equations
    theorem EuclideanGeometry.Sphere.mk_center {P : Type u_2} [MetricSpace P] (c : P) (r : ) :
    { center := c, radius := r }.center = c
    theorem EuclideanGeometry.Sphere.mk_radius {P : Type u_2} [MetricSpace P] (c : P) (r : ) :
    { center := c, radius := r }.radius = r
    @[simp]
    theorem EuclideanGeometry.Sphere.mk_center_radius {P : Type u_2} [MetricSpace P] (s : EuclideanGeometry.Sphere P) :
    { center := s.center, radius := s.radius } = s
    @[simp]
    theorem EuclideanGeometry.Sphere.coe_mk {P : Type u_2} [MetricSpace P] (c : P) (r : ) :
    Metric.sphere { center := c, radius := r }.center { center := c, radius := r }.radius = Metric.sphere c r
    theorem EuclideanGeometry.Sphere.mem_coe {P : Type u_2} [MetricSpace P] {p : P} {s : EuclideanGeometry.Sphere P} :
    p Metric.sphere s.center s.radius p s
    @[simp]
    theorem EuclideanGeometry.Sphere.mem_coe' {P : Type u_2} [MetricSpace P] {p : P} {s : EuclideanGeometry.Sphere P} :
    dist p s.center = s.radius p s
    theorem EuclideanGeometry.mem_sphere {P : Type u_2} [MetricSpace P] {p : P} {s : EuclideanGeometry.Sphere P} :
    p s dist p s.center = s.radius
    theorem EuclideanGeometry.mem_sphere' {P : Type u_2} [MetricSpace P] {p : P} {s : EuclideanGeometry.Sphere P} :
    p s dist s.center p = s.radius
    theorem EuclideanGeometry.subset_sphere {P : Type u_2} [MetricSpace P] {ps : Set P} {s : EuclideanGeometry.Sphere P} :
    ps Metric.sphere s.center s.radius pps, p s
    theorem EuclideanGeometry.dist_of_mem_subset_sphere {P : Type u_2} [MetricSpace P] {p : P} {ps : Set P} {s : EuclideanGeometry.Sphere P} (hp : p ps) (hps : ps Metric.sphere s.center s.radius) :
    dist p s.center = s.radius
    theorem EuclideanGeometry.dist_of_mem_subset_mk_sphere {P : Type u_2} [MetricSpace P] {p : P} {c : P} {ps : Set P} {r : } (hp : p ps) (hps : ps Metric.sphere { center := c, radius := r }.center { center := c, radius := r }.radius) :
    dist p c = r
    theorem EuclideanGeometry.Sphere.ne_iff {P : Type u_2} [MetricSpace P] {s₁ : EuclideanGeometry.Sphere P} {s₂ : EuclideanGeometry.Sphere P} :
    s₁ s₂ s₁.center s₂.center s₁.radius s₂.radius
    theorem EuclideanGeometry.Sphere.center_eq_iff_eq_of_mem {P : Type u_2} [MetricSpace P] {s₁ : EuclideanGeometry.Sphere P} {s₂ : EuclideanGeometry.Sphere P} {p : P} (hs₁ : p s₁) (hs₂ : p s₂) :
    s₁.center = s₂.center s₁ = s₂
    theorem EuclideanGeometry.Sphere.center_ne_iff_ne_of_mem {P : Type u_2} [MetricSpace P] {s₁ : EuclideanGeometry.Sphere P} {s₂ : EuclideanGeometry.Sphere P} {p : P} (hs₁ : p s₁) (hs₂ : p s₂) :
    s₁.center s₂.center s₁ s₂
    theorem EuclideanGeometry.dist_center_eq_dist_center_of_mem_sphere {P : Type u_2} [MetricSpace P] {p₁ : P} {p₂ : P} {s : EuclideanGeometry.Sphere P} (hp₁ : p₁ s) (hp₂ : p₂ s) :
    dist p₁ s.center = dist p₂ s.center
    theorem EuclideanGeometry.dist_center_eq_dist_center_of_mem_sphere' {P : Type u_2} [MetricSpace P] {p₁ : P} {p₂ : P} {s : EuclideanGeometry.Sphere P} (hp₁ : p₁ s) (hp₂ : p₂ s) :
    dist s.center p₁ = dist s.center p₂

    A set of points is cospherical if they are equidistant from some point. In two dimensions, this is the same thing as being concyclic.

    Equations
    Instances For
      theorem EuclideanGeometry.cospherical_def {P : Type u_2} [MetricSpace P] (ps : Set P) :
      EuclideanGeometry.Cospherical ps ∃ (center : P) (radius : ), pps, dist p center = radius

      The definition of Cospherical.

      A set of points is cospherical if and only if they lie in some sphere.

      The set of points in a sphere is cospherical.

      theorem EuclideanGeometry.Cospherical.subset {P : Type u_2} [MetricSpace P] {ps₁ : Set P} {ps₂ : Set P} (hs : ps₁ ps₂) (hc : EuclideanGeometry.Cospherical ps₂) :

      A subset of a cospherical set is cospherical.

      A single point is cospherical.

      theorem EuclideanGeometry.cospherical_pair {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace V] [MetricSpace P] [NormedAddTorsor V P] (p₁ : P) (p₂ : P) :

      Two points are cospherical.

      structure EuclideanGeometry.Concyclic {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace V] [MetricSpace P] [NormedAddTorsor V P] (ps : Set P) :

      A set of points is concyclic if it is cospherical and coplanar. (Most results are stated directly in terms of Cospherical instead of using Concyclic.)

      Instances For
        theorem EuclideanGeometry.Concyclic.subset {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace V] [MetricSpace P] [NormedAddTorsor V P] {ps₁ : Set P} {ps₂ : Set P} (hs : ps₁ ps₂) (h : EuclideanGeometry.Concyclic ps₂) :

        A subset of a concyclic set is concyclic.

        A single point is concyclic.

        theorem EuclideanGeometry.concyclic_pair {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace V] [MetricSpace P] [NormedAddTorsor V P] (p₁ : P) (p₂ : P) :

        Two points are concyclic.

        Any three points in a cospherical set are affinely independent.

        theorem EuclideanGeometry.Cospherical.affineIndependent_of_mem_of_ne {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace P] [NormedAddTorsor V P] {s : Set P} (hs : EuclideanGeometry.Cospherical s) {p₁ : P} {p₂ : P} {p₃ : P} (h₁ : p₁ s) (h₂ : p₂ s) (h₃ : p₃ s) (h₁₂ : p₁ p₂) (h₁₃ : p₁ p₃) (h₂₃ : p₂ p₃) :
        AffineIndependent ![p₁, p₂, p₃]

        Any three points in a cospherical set are affinely independent.

        theorem EuclideanGeometry.Cospherical.affineIndependent_of_ne {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} {p₃ : P} (hs : EuclideanGeometry.Cospherical {p₁, p₂, p₃}) (h₁₂ : p₁ p₂) (h₁₃ : p₁ p₃) (h₂₃ : p₂ p₃) :
        AffineIndependent ![p₁, p₂, p₃]

        The three points of a cospherical set are affinely independent.

        theorem EuclideanGeometry.inner_vsub_vsub_of_mem_sphere_of_mem_sphere {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace P] [NormedAddTorsor V P] {p₁ : P} {p₂ : P} {s₁ : EuclideanGeometry.Sphere P} {s₂ : EuclideanGeometry.Sphere P} (hp₁s₁ : p₁ s₁) (hp₂s₁ : p₂ s₁) (hp₁s₂ : p₁ s₂) (hp₂s₂ : p₂ s₂) :
        inner (s₂.center -ᵥ s₁.center) (p₂ -ᵥ p₁) = 0

        Suppose that p₁ and p₂ lie in spheres s₁ and s₂. Then the vector between the centers of those spheres is orthogonal to that between p₁ and p₂; this is a version of inner_vsub_vsub_of_dist_eq_of_dist_eq for bundled spheres. (In two dimensions, this says that the diagonals of a kite are orthogonal.)

        theorem EuclideanGeometry.eq_of_mem_sphere_of_mem_sphere_of_mem_of_finrank_eq_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace P} [FiniteDimensional s.direction] (hd : Module.finrank s.direction = 2) {s₁ : EuclideanGeometry.Sphere P} {s₂ : EuclideanGeometry.Sphere P} {p₁ : P} {p₂ : P} {p : P} (hs₁ : s₁.center s) (hs₂ : s₂.center s) (hp₁s : p₁ s) (hp₂s : p₂ s) (hps : p s) (hs : s₁ s₂) (hp : p₁ p₂) (hp₁s₁ : p₁ s₁) (hp₂s₁ : p₂ s₁) (hps₁ : p s₁) (hp₁s₂ : p₁ s₂) (hp₂s₂ : p₂ s₂) (hps₂ : p s₂) :
        p = p₁ p = p₂

        Two spheres intersect in at most two points in a two-dimensional subspace containing their centers; this is a version of eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two for bundled spheres.

        theorem EuclideanGeometry.eq_of_mem_sphere_of_mem_sphere_of_finrank_eq_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace P] [NormedAddTorsor V P] [FiniteDimensional V] (hd : Module.finrank V = 2) {s₁ : EuclideanGeometry.Sphere P} {s₂ : EuclideanGeometry.Sphere P} {p₁ : P} {p₂ : P} {p : P} (hs : s₁ s₂) (hp : p₁ p₂) (hp₁s₁ : p₁ s₁) (hp₂s₁ : p₂ s₁) (hps₁ : p s₁) (hp₁s₂ : p₁ s₂) (hp₂s₂ : p₂ s₂) (hps₂ : p s₂) :
        p = p₁ p = p₂

        Two spheres intersect in at most two points in two-dimensional space; this is a version of eq_of_dist_eq_of_dist_eq_of_finrank_eq_two for bundled spheres.

        theorem EuclideanGeometry.inner_pos_or_eq_of_dist_le_radius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace P] [NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ : P} {p₂ : P} (hp₁ : p₁ s) (hp₂ : dist p₂ s.center s.radius) :
        0 < inner (p₁ -ᵥ p₂) (p₁ -ᵥ s.center) p₁ = p₂

        Given a point on a sphere and a point not outside it, the inner product between the difference of those points and the radius vector is positive unless the points are equal.

        theorem EuclideanGeometry.inner_nonneg_of_dist_le_radius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace P] [NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ : P} {p₂ : P} (hp₁ : p₁ s) (hp₂ : dist p₂ s.center s.radius) :
        0 inner (p₁ -ᵥ p₂) (p₁ -ᵥ s.center)

        Given a point on a sphere and a point not outside it, the inner product between the difference of those points and the radius vector is nonnegative.

        theorem EuclideanGeometry.inner_pos_of_dist_lt_radius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace P] [NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ : P} {p₂ : P} (hp₁ : p₁ s) (hp₂ : dist p₂ s.center < s.radius) :
        0 < inner (p₁ -ᵥ p₂) (p₁ -ᵥ s.center)

        Given a point on a sphere and a point inside it, the inner product between the difference of those points and the radius vector is positive.

        theorem EuclideanGeometry.wbtw_of_collinear_of_dist_center_le_radius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace P] [NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ : P} {p₂ : P} {p₃ : P} (h : Collinear {p₁, p₂, p₃}) (hp₁ : p₁ s) (hp₂ : dist p₂ s.center s.radius) (hp₃ : p₃ s) (hp₁p₃ : p₁ p₃) :
        Wbtw p₁ p₂ p₃

        Given three collinear points, two on a sphere and one not outside it, the one not outside it is weakly between the other two points.

        theorem EuclideanGeometry.sbtw_of_collinear_of_dist_center_lt_radius {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace P] [NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ : P} {p₂ : P} {p₃ : P} (h : Collinear {p₁, p₂, p₃}) (hp₁ : p₁ s) (hp₂ : dist p₂ s.center < s.radius) (hp₃ : p₃ s) (hp₁p₃ : p₁ p₃) :
        Sbtw p₁ p₂ p₃

        Given three collinear points, two on a sphere and one inside it, the one inside it is strictly between the other two points.