frequently_top — Mathlib

English

A predicate p on α is frequent with respect to the top filter iff there exists some element x with p(x).

Русский

Наличие частотности для p относительно верхнего фильтра эквивалентно существованию некоторого элемента x with p(x).

LaTeX

$$$\\left(\\exists S\\subseteq \\alpha\\,(S \\in \\top \\wedge \\forall x\\in S,\\ p(x))\\right) \\iff \\exists x\\in \\alpha,\\ p(x)$$$

Lean4

@[simp]
theorem frequently_top {p : α → Prop} : (∃ᶠ x in ⊤, p x) ↔ ∃ x, p x := by simp [Filter.Frequently]

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