frequently_iff_neBot — Mathlib

English

For any filter l and proposition p, the frequent predicate on l is equivalent to the nontrivial intersection of l with the principal filter on p.

Русский

Для любого фильтра l и про позиция p, частотность на l эквивалентна не тривиальному пересечению l с простейшим фильтром на p.

LaTeX

$$$ (\exists^\! x \in l, p(x)) \leftrightarrow NeBot (l \cap 𝓟\{x \mid p(x)\}) $$$

Lean4

theorem frequently_iff_neBot {l : Filter α} {p : α → Prop} : (∃ᶠ x in l, p x) ↔ NeBot (l ⊓ 𝓟 {x | p x}) := by
  rw [neBot_iff, Ne, inf_principal_eq_bot]; rfl

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