frequently_iff — Mathlib

English

For any filter f and predicate P, (∃ᶠ x in f, P(x)) holds iff for every set U in f there exists x ∈ U with P(x).

Русский

Для любого фильтра f и предиката P: (∃ᶠ x in f, P(x)) выполняется тогда и только тогда, когда для каждого множества U ∈ f существует x ∈ U такое, что P(x).

LaTeX

$$$ (\exists^\! x \in f, P(x)) \iff \forall U, U \in f \rightarrow \exists x \in U, P(x) $$$

Lean4

theorem frequently_iff {f : Filter α} {P : α → Prop} : (∃ᶠ x in f, P x) ↔ ∀ {U}, U ∈ f → ∃ x ∈ U, P x :=
  by
  simp only [frequently_iff_forall_eventually_exists_and, @and_comm (P _)]
  rfl

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