eventually_cofinite — Mathlib

English

For any predicate p on α, the statement 'p holds eventually with respect to μ.cofinite' is equivalent to the μ-measure of the set where p is false being finite.

Русский

Для любого предиката p на α утверждение «p истинно почти всюду в отношении μ.cofinite» эквивалентно тому, что мера множества {x : ¬p(x)} по μ конечна.

LaTeX

$$$(\forall^\infty x \text{ in } \mu.cofinite, p(x)) \;\iff\; \mu\{x \mid \lnot p(x)\} < \infty$$$

Lean4

theorem eventually_cofinite {p : α → Prop} : (∀ᶠ x in μ.cofinite, p x) ↔ μ {x | ¬p x} < ∞ :=
  Iff.rfl

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