affineCombination_apply_const — Mathlib

English

If two weight families w1,w2 agree on s and two point families p1,p2 agree on s, then the resulting affine combinations agree.

Русский

Если две семьи весов совпадают на s и две семьи точек совпадают на s, то полученные аффинные комбинации совпадают.

LaTeX

$$$ s.affineCombination k p_1 w_1 = s.affineCombination k p_2 w_2 $ under$ hw$ и$ hp $.$$

Lean4

/-- The value of `affineCombination`, where the given points are equal. -/
@[simp]
theorem affineCombination_apply_const (w : ι → k) (p : P) (h : ∑ i ∈ s, w i = 1) :
    s.affineCombination k (fun _ => p) w = p := by
  rw [affineCombination_apply, s.weightedVSubOfPoint_apply_const, h, one_smul, vsub_vadd]

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