English
For a non-dependent codomain, updating a function f at a' with b yields a function whose value at a is b when a = a' and f a otherwise.
Русский
Для ненезависимого по аргументу кодом вида обновления функции: обновление в точке a' значением b дает функцию, у которой значение в a равно b если a = a', иначе равно f(a).
LaTeX
$$$\\mathrm{update}\\ f\\ a'\\ b\\ a = \\begin{cases} b, & a = a' \\\\ f\\ a, & a \\neq a' \\end{cases}$$$
Lean4
/-- On non-dependent functions, `Function.update` can be expressed as an `ite` -/
theorem update_apply {β : Sort*} (f : α → β) (a' : α) (b : β) (a : α) : update f a' b a = if a = a' then b else f a :=
by rcases Decidable.eq_or_ne a a' with rfl | hne <;> simp [*]
