Eventually — Mathlib

English

The predicate Eventually p f is defined by the membership of the set {x | p(x)} in f.

Русский

Предикат Eventually p f определяется принадлежностью множества {x | p(x)} фильтру f.

LaTeX

$$$\\mathrm{Eventually}(p,f) \\;:=\\; \\{x \\mid p(x)\\} \\in f$$$

Lean4

/-- `f.Eventually p` or `∀ᶠ x in f, p x` mean that `{x | p x} ∈ f`. E.g., `∀ᶠ x in atTop, p x`
means that `p` holds true for sufficiently large `x`. -/
protected def Eventually (p : α → Prop) (f : Filter α) : Prop :=
  {x | p x} ∈ f

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