affineCombination_touchpointWeights

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

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