coord_apply — Mathlib

English

If i ∈ s and the weights w sum to 1, the i-th coordinate of the affine combination equals w_i.

Русский

Если i ∈ s и веса w суммируются в 1, i-я координата аффинного сочетания равна w_i.

LaTeX

$$$hi \in s \land s.sum w = 1 \Rightarrow b.coord i (s.affineCombination k b w) = w i$$$

Lean4

theorem coord_apply [DecidableEq ι] (i j : ι) : b.coord i (b j) = if i = j then 1 else 0 := by
  rcases eq_or_ne i j with h | h <;> simp [h]

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