frequently_cofinite_iff_infinite — Mathlib

English

A property p on α is frequently true in the cofinite filter if and only if the set {x | p(x)} is infinite.

Русский

Свойство p на α часто выполняется в кофинитном фильтре тогда и только тогда, когда множество {x | p(x)} бесконечно.

LaTeX

$$$(\exists^\infty x \in \operatorname{cofinite}} p(x)) \iff {x \mid p(x)} \text{ Infinite}$$$

Lean4

theorem frequently_cofinite_iff_infinite {p : α → Prop} : (∃ᶠ x in cofinite, p x) ↔ Set.Infinite {x | p x} := by
  simp only [Filter.Frequently, eventually_cofinite, not_not, Set.Infinite]

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