frequently_iff_eventually — Mathlib

English

In an ultrafilter, being frequent for p is equivalent to eventually p.

Русский

В ульрафильтре частотность для p эквивалентна пределающимся (eventually) условию p.

LaTeX

$$$\\\\forall {\\\\alpha} \\\\forall {f \\\\in \\\\mathrm{Ultrafilter}(\\\\alpha)} {p \\\\colon \\\\alpha \\\\to \\\\mathrm{Prop}}, \\\\exists^\\\\mathrm{freq} x \\\\in f \, p(x) \\\\Leftrightarrow \\\\forall_{x \in f} \\\\; p(x)$$$

Lean4

@[simp]
theorem frequently_iff_eventually : (∃ᶠ x in f, p x) ↔ ∀ᶠ x in f, p x :=
  compl_notMem_iff

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