circumcenter_eq_affineCombination_of_pointsWithCircumcenter

English

The circumcenter equals the affine combination of pointsWithCircumcenter using circumcenterWeightsWithCircumcenter.

Русский

Центр окружности равен аффинной комбинации точек с использованием circumcenterWeightsWithCircumcenter.

LaTeX

$$$s.circumcenter = (\univ : Finset (PointsWithCircumcenterIndex n)).affineCombination\; s.pointsWithCircumcenter\; (circumcenterWeightsWithCircumcenter n)$$$

Lean4

/-- The circumcenter of a simplex, in terms of `pointsWithCircumcenter`. -/
theorem circumcenter_eq_affineCombination_of_pointsWithCircumcenter {n : ℕ} (s : Simplex ℝ P n) :
    s.circumcenter =
      (univ : Finset (PointsWithCircumcenterIndex n)).affineCombination ℝ s.pointsWithCircumcenter
        (circumcenterWeightsWithCircumcenter n) :=
  by
  rw [← pointsWithCircumcenter_eq_circumcenter]
  symm
  refine affineCombination_of_eq_one_of_eq_zero _ _ _ (mem_univ _) rfl ?_
  rintro ⟨i⟩ _ hn <;> tauto

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