English
For a fixed f, a, b and a predicate p on pairs (a, β a), the property p holds for the updated function at every input x iff p holds at the updated coordinate and holds for all other coordinates with the original values.
Русский
Для данного f, a, b и предиката p на паре (a, β(a)), свойство p применимо к обновлённой функции на всех аргументах тогда и только тогда, когда оно выполняется на обновлённой координате и для всех остальных x выполняется p на (x, f(x)).
LaTeX
$$$\\forall x,\\ p{x}{x}(\\mathrm{update}\\ f\\ a\\ b\\ x) \\iff p\\ a\\ b \\wedge \\forall x, x \\neq a \\rightarrow p\\ x\\ (f\\ x)$$$
Lean4
theorem forall_update_iff (f : ∀ a, β a) {a : α} {b : β a} (p : ∀ a, β a → Prop) :
(∀ x, p x (update f a b x)) ↔ p a b ∧ ∀ x, x ≠ a → p x (f x) :=
by
rw [← and_forall_ne a, update_self]
simp +contextual
