eventuallyEq_iff_exists_mem — Mathlib

English

Equality almost everywhere is equivalent to the existence of a set in the filter on which f and g are equal pointwise.

Русский

Эквивалентность почти всюду равна существованию множества в фильтре, на котором f и g равны по точкам.

LaTeX

$$$f =^{{l}} g \\iff \\exists S \\in l, \\forall x\\in S,\\ f(x)=g(x)$$$

Lean4

theorem eventuallyEq_iff_exists_mem {l : Filter α} {f g : α → β} : f =ᶠ[l] g ↔ ∃ s ∈ l, EqOn f g s :=
  eventually_iff_exists_mem

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