frequently_atTop_iff_infinite — Mathlib

English

For p : Natural → Prop, ∃ᶠ n in atTop, p(n) iff {n | p(n)} is infinite.

Русский

Для p: ℕ → Prop, ∃ᶠ n в atTop, p(n) тогда и только тогда, когда множество {n | p(n)} бесконечно.

LaTeX

$$$\\exists\\!^{\\mathrm{fin}} n \\; p(n) \\text{ in } atTop \\iff \\{n \\mid p(n)\\} \\text{ is infinite}$$$

Lean4

theorem frequently_atTop_iff_infinite {p : ℕ → Prop} : (∃ᶠ n in atTop, p n) ↔ Set.Infinite {n | p n} := by
  rw [← Nat.cofinite_eq_atTop, frequently_cofinite_iff_infinite]

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