eq_circumcenter_of_dist_eq — Mathlib

English

For a 1-simplex, the circumcenter equals the centroid of its two vertices.

Русский

Для 1-симплекса центр окружности совпадает с центроидом двух вершин.

LaTeX

$$$s.circumcenter = \\mathrm{centroid}(s.points)$ when $s$ is a 1-simplex.$$

Lean4

/-- Given a point in the affine span from which all the points are
equidistant, that point is the circumcenter. -/
theorem eq_circumcenter_of_dist_eq {n : ℕ} (s : Simplex ℝ P n) {p : P} (hp : p ∈ affineSpan ℝ (Set.range s.points))
    {r : ℝ} (hr : ∀ i, dist (s.points i) p = r) : p = s.circumcenter :=
  by
  have h := s.circumsphere_unique_dist_eq.2 ⟨p, r⟩
  simp only [hp, hr, forall_const, subset_sphere (s := ⟨p, r⟩), Sphere.ext_iff, Set.forall_mem_range, mem_sphere,
    true_and] at h
  exact h.1

Похожие утверждения