integrableOn_add_measure — Mathlib

English

The integrability of f on s with respect to μ + ν is equivalent to the conjunction of integrability on μ and on ν.

Русский

Интегрируемость f на s по μ+ν эквивалентна сочетанию интегрируемости по μ и по ν.

LaTeX

$$IntegrableOn(f,s,μ+ν) ⇔ IntegrableOn(f,s,μ) ∧ IntegrableOn(f,s,ν)$$

Lean4

@[simp]
theorem integrableOn_add_measure [PseudoMetrizableSpace ε] :
    IntegrableOn f s (μ + ν) ↔ IntegrableOn f s μ ∧ IntegrableOn f s ν :=
  ⟨fun h => ⟨h.mono_measure (Measure.le_add_right le_rfl), h.mono_measure (Measure.le_add_left le_rfl)⟩, fun h =>
    h.1.add_measure h.2⟩

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