erase_apply — Mathlib

English

For any a, a', f, the value (f.erase a) a' equals 0 if a' = a and equals f a' otherwise.

Русский

Для любых a, a' и f значение (f.erase a) a' равно 0 при a' = a и равно f a' при a' ≠ a.

LaTeX

$$$(f.erase a) a' = \begin{cases} 0, & a' = a \\ f(a'), & a' \neq a \end{cases}$$$

Lean4

theorem erase_apply [DecidableEq α] {a a' : α} {f : α →₀ M} : f.erase a a' = if a' = a then 0 else f a' :=
  by
  rw [erase, coe_mk]
  simp only [ite_eq_ite]

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