sigmaFiniteSet — Mathlib

English

For an AEFinStronglyMeasurable function f, sigmaFiniteSet(f) is the chosen measurable set witnessing the sigma-finiteness of μ|t and the a.e. vanishing of f on tᶜ.

Русский

Для AEFinStronglyMeasurable функции f множество sigmaFiniteSet(f) — выборочное измеримое множество, доказывающее сигма-конечность μ|t и равенство f нулю почти всюду на tᶜ.

LaTeX

$$$\\text{sigmaFiniteSet}(f) \\text{ is measurable and } f =^{\\mathrm{a}}_{\\mu|_{\\sigmaFiniteSet(f)^c}} 0 \\land \\Sigma\\text{-finite}(\\mu|_{\\sigmaFiniteSet(f)})$$$

Lean4

/-- A measurable set `t` such that `f =ᵐ[μ.restrict tᶜ] 0` and `sigma_finite (μ.restrict t)`. -/
def sigmaFiniteSet (hf : AEFinStronglyMeasurable f μ) : Set α :=
  hf.exists_set_sigmaFinite.choose

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