circumsphere_eq_of_cospherical — Mathlib

English

All n-simplices among cospherical points in full space have the same circumsphere.

Русский

Все n-мерные симплексы из кососферических точек во всей плоскости имеют одну и ту же circumsphere.

LaTeX

$$$\exists S \in \text{Sphere } P, \forall sx : \text{Simplex } \mathbb{R} P\, n,\; (\text{range } sx.points \subseteq ps) \Rightarrow sx.circumsphere = S$$$

Lean4

/-- Two n-simplices among cospherical points in n-space have the same
circumsphere. -/
theorem circumsphere_eq_of_cospherical {ps : Set P} {n : ℕ} [FiniteDimensional ℝ V] (hd : finrank ℝ V = n)
    (hc : Cospherical ps) {sx₁ sx₂ : Simplex ℝ P n} (hsx₁ : Set.range sx₁.points ⊆ ps)
    (hsx₂ : Set.range sx₂.points ⊆ ps) : sx₁.circumsphere = sx₂.circumsphere :=
  by
  rcases exists_circumsphere_eq_of_cospherical hd hc with ⟨r, hr⟩
  rw [hr sx₁ hsx₁, hr sx₂ hsx₂]

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