circumcenter_eq_point — Mathlib

English

For a 0-simplex, the circumcenter equals its unique vertex.

Русский

Для 0-симплексa circumcenter совпадает с единственной вершиной.

LaTeX

$$$(s : Simplex ℝ P 0).circumcenter = (s.points 0)$$$

Lean4

/-- The circumcenter of a 0-simplex equals its unique point. -/
theorem circumcenter_eq_point (s : Simplex ℝ P 0) (i : Fin 1) : s.circumcenter = s.points i :=
  by
  have h := s.circumcenter_mem_affineSpan
  have : Unique (Fin 1) := ⟨⟨0, by decide⟩, fun a => by simp only [Fin.eq_zero]⟩
  simp only [Set.range_unique, AffineSubspace.mem_affineSpan_singleton] at h
  rw [h]
  congr
  simp only [eq_iff_true_of_subsingleton]

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