ae_iff_of_countable — Mathlib

English

In a countable domain, (∀ᵐ x, p x) is equivalent to ∀ x, μ{x} ≠ 0 → p x.

Русский

В счётном пространстве (∀ᵐ x, p x) эквивалентно ∀ x, μ{x} ≠ 0 → p x.

LaTeX

$$$\text{[Countable }\alpha] \; (\forall^{\text{ae}} x, p x) \iff \forall x, \mu\{x\} \neq 0 \to p x$$$

Lean4

theorem ae_iff_of_countable [Countable α] {p : α → Prop} : (∀ᵐ x ∂μ, p x) ↔ ∀ x, μ { x } ≠ 0 → p x :=
  by
  rw [ae_iff, measure_null_iff_singleton]
  exacts [forall_congr' fun _ ↦ not_imp_comm, Set.to_countable _]

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