coeff_update_apply — Mathlib

English

For any index a', the coefficient of a' in f.update a b is b if a' = a, and is f.coeff(a') otherwise.

Русский

Для любого индекса a' коэффициент f.update a b в позиции a' равен b, если a' = a, и равен f.coeff(a') иначе.

LaTeX

$$$(f.update\\ a\\ b).\\text{coeff}\\ a' = \\begin{cases} b, & a' = a \\\\ f.\\text{coeff}\\ a', & a' \\neq a. \\end{cases}$$$

Lean4

theorem coeff_update_apply [DecidableEq α] : (f.update a b).coeff a' = if a' = a then b else f.coeff a' := by
  rw [coeff_update, Function.update_apply]

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