exists_circumsphere_eq_of_cospherical

English

Two n-simplices among cospherical points have the same circumsphere.

Русский

Даны два n-симплекса кососферических точек, их circumsphere совпадает.

LaTeX

$$$\forall \{sx_1,sx_2\} : \text{Simplex } \mathbb{R} P\, n,\; (\text{range } sx_1.points \subseteq ps) \land (\text{range } sx_2.points \subseteq ps) \Rightarrow sx_1.circumsphere = sx_2.circumsphere$$$

Lean4

/-- All n-simplices among cospherical points in n-space have the same
circumsphere. -/
theorem exists_circumsphere_eq_of_cospherical {ps : Set P} {n : ℕ} [FiniteDimensional ℝ V] (hd : finrank ℝ V = n)
    (hc : Cospherical ps) : ∃ c : Sphere P, ∀ sx : Simplex ℝ P n, Set.range sx.points ⊆ ps → sx.circumsphere = c :=
  by
  haveI : Nonempty (⊤ : AffineSubspace ℝ P) := Set.univ.nonempty
  rw [← finrank_top, ← direction_top ℝ V P] at hd
  refine exists_circumsphere_eq_of_cospherical_subset ?_ hd hc
  exact Set.subset_univ _

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