frequently_mem_iff_neBot — Mathlib

English

For a filter l and a subset s, p(x) := x ∈ s holds frequently with respect to l if and only if l ∩ 𝓟 s is nontrivial.

Русский

Для фильтра l и подмножества s частотность x ∈ s по l эквивалентна тому, что пересечение фильтра l с простейшим фильтром на s не тривиально.

LaTeX

$$$ (\exists^\! x \in l, x \in s) \leftrightarrow NeBot (l \cap 𝓟 s) $$$

Lean4

theorem frequently_mem_iff_neBot {l : Filter α} {s : Set α} : (∃ᶠ x in l, x ∈ s) ↔ NeBot (l ⊓ 𝓟 s) :=
  frequently_iff_neBot

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