update_eventuallyEq — Mathlib

English

Given a function f and a point a, updating f at a to value b yields a function that equals f outside {a} on a cofinite set.

Русский

Замена значения функции в точке a на b совпадает с исходной функцией на множестве, у которого исключения составляют одноточечное множество.

LaTeX

$$$\\text{update } f\\ a\\ b =^\\text{E} f$ on $\\mathcal{P}({a})^c$$$

Lean4

theorem update_eventuallyEq [DecidableEq α] (f : α → β) (a : α) (b : β) : Function.update f a b =ᶠ[𝓟 { a }ᶜ] f := by
  filter_upwards [mem_principal_self _] with u hu using Function.update_of_ne hu _ _

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