Theorems · Theorem · geometry

EuclideanGeometry.eq_or_eq_reflection_of_dist_eq

∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} {s : Affine.Simplex ℝ P n} {p p₁ p₂ : P} {r : ℝ},
  p₁ ∈ affineSpan ℝ (insert p (Set.range s.points)) →
    p₂ ∈ affineSpan ℝ (insert p (Set.range s.points)) →
      (∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r) →
        (∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r) →
          p₁ = p₂ ∨ p₁ = (EuclideanGeometry.reflection (affineSpan ℝ (Set.range s.points))) p₂

Suppose all distances from p₁ and p₂ to the points of a simplex are equal, and that p₁ and p₂ lie in the affine span of p with the vertices of that simplex. Then p₁ and p₂ are equal or reflections of each other in the affine span of the vertices of the simplex.

Defined in

Mathlib.Geometry.Euclidean.Circumcenter

Cited by

0 results in Mathlib

Foundations

Depth 193 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsor