ae_count_iff — Mathlib

English

For any predicate p on α, almost every x with respect to count satisfies p x iff p x holds for all x.

Русский

Для произвольного свойства p на α, почти наверняка при счётной мере, выполняется p x для всех x.

LaTeX

$$$(\forall x, p(x)) \iff (\forallᵐ x \partial count, p(x))$$$

Lean4

@[simp]
theorem ae_count_iff {p : α → Prop} : (∀ᵐ x ∂count, p x) ↔ ∀ x, p x :=
  by
  refine ⟨fun h x ↦ ?_, ae_of_all _⟩
  rw [ae_iff, count_eq_zero_iff] at h
  by_contra hx
  rwa [← mem_empty_iff_false x, ← h]

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