add_measure — Mathlib

English

If f is AEMeasurable with respect to μ and ν, then f is AEMeasurable with respect to μ + ν. In other words, a.e. measurability is preserved under addition of measures.

Русский

Если f измеримо почти всюду относительно μ и ν, то f измеримо почти всюду относительно μ + ν. То есть a.e. измеримость сохраняется при сложении мер.

LaTeX

$$$$ AEMeasurable f \\mu \\quad\\text{and}\\quad AEMeasurable f \\nu \\Rightarrow AEMeasurable f (\\mu + \\nu). $$$$

Lean4

@[measurability]
theorem add_measure {f : α → β} (hμ : AEMeasurable f μ) (hν : AEMeasurable f ν) : AEMeasurable f (μ + ν) :=
  aemeasurable_add_measure_iff.2 ⟨hμ, hν⟩

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