add_measure — Mathlib

English

If f is AEStronglyMeasurable for each μ.restrict(s_i), then it is AEStronglyMeasurable for μ.restrict(∪ s_i).

Русский

Если функция f сильнос-измерима по каждой мере μ, ограниченной множеством s_i, то она сильнос-измерима и на объединении всех s_i.

LaTeX

$$$\forall i,\; \text{AEStronglyMeasurable}(f, μ.restrict(s_i)) \Rightarrow \text{AEStronglyMeasurable}(f, μ.restrict(\bigcup_i s_i)).$$$

Lean4

@[fun_prop, measurability]
theorem add_measure [PseudoMetrizableSpace β] {ν : Measure α} {f : α → β} (hμ : AEStronglyMeasurable f μ)
    (hν : AEStronglyMeasurable f ν) : AEStronglyMeasurable f (μ + ν) :=
  aestronglyMeasurable_add_measure_iff.2 ⟨hμ, hν⟩

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