English
The i-th vertex s.points i equals an affine combination of the point set s.pointsWithCircumcenter with weights given by pointWeightsWithCircumcenter i.
Русский
i-я вершина s.points i равна аффинной комбинации точек s.pointsWithCircumcenter с весами pointWeightsWithCircumcenter i.
LaTeX
$$$s.points\,i = (\univ : Finset (PointsWithCircumcenterIndex n)).affineCombination\; s.pointsWithCircumcenter\; (pointWeightsWithCircumcenter i)$$$
Lean4
/-- A single vertex, in terms of `pointsWithCircumcenter`. -/
theorem point_eq_affineCombination_of_pointsWithCircumcenter {n : ℕ} (s : Simplex ℝ P n) (i : Fin (n + 1)) :
s.points i =
(univ : Finset (PointsWithCircumcenterIndex n)).affineCombination ℝ s.pointsWithCircumcenter
(pointWeightsWithCircumcenter i) :=
by
rw [← pointsWithCircumcenter_point]
symm
refine affineCombination_of_eq_one_of_eq_zero _ _ _ (mem_univ _) (by simp [pointWeightsWithCircumcenter]) ?_
intro i hi hn
cases i
· have h : _ ≠ i := fun h => hn (h ▸ rfl)
simp [pointWeightsWithCircumcenter, h]
· rfl
