EventuallyEq — Mathlib

English

Two functions f and g are eventually equal along a filter l if the set of x with f(x) = g(x) belongs to l.

Русский

Две функции f и g эквивалентны в пределе вдоль фильтра l, если множество {x | f(x) = g(x)} принадлежит l.

LaTeX

$$$\\mathrm{EventuallyEq}(l,f,g) \\iff \\forall^{\\infty} x \\in l,\\ f(x)=g(x)$$$

Lean4

/-- Two functions `f` and `g` are *eventually equal* along a filter `l` if the set of `x` such that
`f x = g x` belongs to `l`. -/
def EventuallyEq (l : Filter α) (f g : α → β) : Prop :=
  ∀ᶠ x in l, f x = g x

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