coe_update — Mathlib

English

The underlying function of f.update a b equals Function.update of the underlying function of f by a and b.

Русский

Опорная функция f.update(a,b) равна функции-обертке Function.update, применяемой к базовой функции f.

LaTeX

$$$\mathrm{coe}(f.update(a,b)) = \mathrm{Function.update}(\mathrm{coe}(f), a, b)$$$

Lean4

@[simp, norm_cast]
theorem coe_update [DecidableEq α] : (f.update a b : α → M) = Function.update f a b :=
  by
  delta update Function.update
  ext
  dsimp
  split_ifs <;> simp

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