Theorems · Definition · general topology

Filter.Frequently

{α : Type u_1} → (α → Prop) → Filter α → Prop

f.Frequently p or ∃ᶠ x in f, p x mean that {x | ¬p x} ∉ f. E.g., ∃ᶠ x in atTop, p x means that there exist arbitrarily large x for which p holds true.

Defined in

Mathlib.Order.Filter.Defs

Cited by

414 results in Mathlib

Foundations

Depth 6 from the axioms, rests on 14 definitions · uses no axioms