frequently_principal — Mathlib

English

In the principal filter on a set a, p holds frequently exactly when there exists x in a with p(x).

Русский

В принципиальном фильтре на множество a частотность p эквивалентна существованию элемента x в a such that p(x).

LaTeX

$$$\\left(\\existsᶠ x\\in 𝓟 a,\\ p(x)\\right) \\iff \\exists x\\in a,\\ p(x)$$$

Lean4

@[simp]
theorem frequently_principal {a : Set α} {p : α → Prop} : (∃ᶠ x in 𝓟 a, p x) ↔ ∃ x ∈ a, p x := by
  simp [Filter.Frequently, not_forall]

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