English
The touchpoint is obtained by applying the affine combination with the touchpoint weights to the vertices.
Русский
Аффинные сочетания точек касания сохраняют равенство соответствующих аффинных сочетаний вершин.
LaTeX
$$$ (\text{affineCombination}\,\text{Real}\, s.points) (\text{touchpointWeights}(\text{signs}, i)) = s.touchpoint(\text{signs}, i) $$$
Lean4
@[simp]
theorem affineCombination_touchpointWeights (signs : Finset (Fin (n + 1))) (i : Fin (n + 1)) :
Finset.univ.affineCombination ℝ s.points (s.touchpointWeights signs i) = s.touchpoint signs i :=
(eq_affineCombination_of_mem_affineSpan_of_fintype (s.touchpoint_mem_affineSpan_simplex signs i)).choose_spec.2.symm