ae_eq_univ_iff_measure_eq — Mathlib

English

Let μ be finite with a NullMeasurableSet s. Then s equals the universe μ-a.e. if and only if μ(s) = μ(univ).

Русский

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

LaTeX

$$$(\mathrm{NullMeasurableSet}(s, \mu)) \Rightarrow (s =_{\mu} \mathrm{univ} \iff \mu(s) = \mu(\mathrm{univ}))$$

Lean4

theorem ae_eq_univ_iff_measure_eq [IsFiniteMeasure μ] (hs : NullMeasurableSet s μ) : s =ᵐ[μ] univ ↔ μ s = μ univ :=
  ⟨measure_congr, fun h ↦ ae_eq_of_subset_of_measure_ge (subset_univ _) h.ge hs (measure_ne_top _ _)⟩

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