update_eventuallyEq_cofinite — Mathlib

English

With a decidable equality, update f at a to b is eventually equal to f on cofinitely many points.

Русский

При разрешимой эквивалентности точка a обновленного f совпадает с f на кофинитной мощности точек.

LaTeX

$$$\\text{update}(f,a,b) =^\\!_{\\text{cofinite}} f$$$

Lean4

theorem update_eventuallyEq_cofinite [DecidableEq α] (f : α → β) (a : α) (b : β) :
    Function.update f a b =ᶠ[cofinite] f :=
  (Function.update_eventuallyEq f a b).filter_mono (by simp)

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