eventually_cofinite — Mathlib

English

Let p be a property on α. The statement that p holds eventually in the cofinite filter is equivalent to the complement set {x | ¬p(x)} being finite.

Русский

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

LaTeX

$$$(\forall x \text{ in cofinite}, p(x)) \iff (\{x \mid \neg p(x)\}).Finite$$$

Lean4

@[simp]
theorem eventually_cofinite {p : α → Prop} : (∀ᶠ x in cofinite, p x) ↔ {x | ¬p x}.Finite :=
  Iff.rfl

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