update_eq_iff — Mathlib

English

Two functions are equal if and only if they agree at the updated argument and agree elsewhere; equivalently, update f a b equals g iff b = g a and f x = g x for all x ≠ a.

Русский

Две функции равны тогда и только тогда, когда они совпадают в обновляемой координате и вне её; эквивалентно, update f a b = g iff b = g a и для всех x ≠ a выполняется f x = g x.

LaTeX

$$$update\\ f\\ a\\ b = g \\iff b = g\\ a \\wedge \\forall x \\neq a,\\ f\\ x = g\\ x$$$

Lean4

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

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