add_measure — Mathlib

English

If f is integrable on s with respect to μ and with respect to ν, then f is integrable on s with respect to μ + ν.

Русский

Если f интегрируем на s по мере μ и по мере ν, то она интегрируема на s по мере μ + ν.

LaTeX

$$(IntegrableOn f s μ) ∧ (IntegrableOn f s ν) ⇒ IntegrableOn f s (μ + ν)$$

Lean4

theorem add_measure [PseudoMetrizableSpace ε] (hμ : IntegrableOn f s μ) (hν : IntegrableOn f s ν) :
    IntegrableOn f s (μ + ν) := by delta IntegrableOn; rw [Measure.restrict_add]; exact hμ.integrable.add_measure hν

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