ae_iff_measure_eq — Mathlib

English

Let μ be finite and let p be a predicate with NullMeasurableSet{a : α | p a}. Then μ-almost everywhere p holds iff μ{a : α | p a} = μ(univ).

Русский

Пусть μ конечна и p — предикат, для которого {a | p a} нуль-измеримо. Тогда μ-почти наверняка p верно тогда и только тогда, когда μ{a | p a} = μ(univ).

LaTeX

$$$(\text{NullMeasurableSet}(\{a \mid p a\}, \mu)) \Rightarrow \left( (\forall a, p a) \text{ μ-a.e. } \right) \iff \mu(\{a \mid p a\}) = \mu(\mathrm{univ})$$$

Lean4

theorem ae_iff_measure_eq [IsFiniteMeasure μ] {p : α → Prop} (hp : NullMeasurableSet {a | p a} μ) :
    (∀ᵐ a ∂μ, p a) ↔ μ {a | p a} = μ univ := by rw [← ae_eq_univ_iff_measure_eq hp, eventuallyEq_univ, eventually_iff]

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