ae_eq_zero_compl — Mathlib

English

For AEFinStronglyMeasurable f, f equals 0 almost everywhere on the complement of sigmaFiniteSet(f) with respect to μ.

Русский

Для AEFinStronglyMeasurable f, функция равна нулю почти всюду на означении комплемента σFiniteSet(f) относительно μ.

LaTeX

$$$f =^{\\mathrm{a}}_{\\mu|_{(\\sigmaFiniteSet(f))^c}} 0$$$

Lean4

theorem ae_eq_zero_compl (hf : AEFinStronglyMeasurable f μ) : f =ᵐ[μ.restrict hf.sigmaFiniteSetᶜ] 0 :=
  hf.exists_set_sigmaFinite.choose_spec.2.1

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