measurable_of_complete — Mathlib

English

If s is NullMeasurableSet with respect to μ and μ is complete, then s is measurable.

Русский

Если s является нулевой измеряемостью множества относительно μ и μ полна, то s измеримо.

LaTeX

$$$\mathrm{NullMeasurableSet}(s,\mu) \Rightarrow \mathrm{MeasurableSet}(s)$, assuming $\mu$ is complete.$$

Lean4

theorem measurable_of_complete (hs : NullMeasurableSet s μ) [μ.IsComplete] : MeasurableSet s :=
  diff_diff_cancel_left (subset_toMeasurable μ s) ▸
    (measurableSet_toMeasurable _ _).diff
      (measurableSet_of_null (ae_le_set.1 <| EventuallyEq.le (NullMeasurableSet.toMeasurable_ae_eq hs)))

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