update_of_ne — Mathlib

English

If a ≠ a', then updating a function f at a' to a value v yields a function whose value at every input a ≠ a' remains f a.

Русский

Если a ≠ a', то обновление функции f в точке a' значением v дает такую же функцию, как и f, в каждой точке a, для которой a ≠ a'.

LaTeX

$$$a \\neq a' \\Rightarrow (update\\ f\\ a'\\ v\\ a) = f\\ a$$$

Lean4

@[simp]
theorem update_of_ne {a a' : α} (h : a ≠ a') (v : β a') (f : ∀ a, β a) : update f a' v a = f a :=
  dif_neg h

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