affineCombination_congr — Mathlib

English

An affine combination over the image of an embedding equals the affine combination with the same points and weights precomposed with the embedding.

Русский

Аффинная комбинация над образа вложения равна аффинной комбинации с теми же точками и весами, предварительно отображенными через вложение.

LaTeX

$$$ (s_2.map e).affineCombination k p w = s_2.affineCombination k (p \circ e) (w \circ e) $$$

Lean4

/-- `affineCombination` gives equal results for two families of weights and two families of
points that are equal on `s`. -/
theorem affineCombination_congr {w₁ w₂ : ι → k} (hw : ∀ i ∈ s, w₁ i = w₂ i) {p₁ p₂ : ι → P}
    (hp : ∀ i ∈ s, p₁ i = p₂ i) : s.affineCombination k p₁ w₁ = s.affineCombination k p₂ w₂ := by
  simp_rw [affineCombination_apply, s.weightedVSubOfPoint_congr hw hp]

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