eq_update_iff — Mathlib

English

For all a, b, f, g, we have g = update f a b iff g a = b and g x = f x for all x ≠ a.

Русский

Для любых a, b, f, g имеет место g = update f a b тогда и только тогда, когда g a = b и для всех x ≠ a выполняется g x = f x.

LaTeX

$$$g = \\mathrm{update}\\ f\\ a\\ b \\iff g\\ a = b \\wedge \\forall x, x \\neq a \\rightarrow g\\ x = f\\ x$$$

Lean4

theorem eq_update_iff {a : α} {b : β a} {f g : ∀ a, β a} : g = update f a b ↔ g a = b ∧ ∀ x ≠ a, g x = f x :=
  funext_iff.trans <| forall_update_iff _ fun x y ↦ g x = y

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