eventuallyEq — Mathlib

English

If two functions f,g are equal on a set s, then they are eventually equal on the principal filter of s.

Русский

Если две функции f и g равны на множестве s, то они являются почти где-тогда на принципиальном фильтре s.

LaTeX

$$$$ \\text{EventualEq}(f,g,\\mathcal{P}s) = \\text{true} $$$$

Lean4

theorem eventuallyEq {α β} {s : Set α} {f g : α → β} (h : EqOn f g s) : f =ᶠ[𝓟 s] g :=
  h

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