eventually_iff — Mathlib

English

For any f and predicate P on α, (∀ᶠ x in f, P x) holds if and only if the set {x | P x} belongs to f.

Русский

Для фильтра f и предиката P на α выполняется: (∀ᶠ x ∈ f, P x) тогда и только тогда, когда множество {x | P x} принадлежит f.

LaTeX

$$$(\\forallᶠ x ∈ f, P x) \\iff \\{x \\mid P x\\} \\in f$$$

Lean4

theorem eventually_iff {f : Filter α} {P : α → Prop} : (∀ᶠ x in f, P x) ↔ {x | P x} ∈ f :=
  Iff.rfl

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