Theorems · Theorem · measure theory

MeasureTheory.integrable_add_iff_integrable_right

∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f g : α → β}, MeasureTheory.Integrable f μ → (MeasureTheory.Integrable (f + g) μ ↔ MeasureTheory.Integrable g μ)

if f is integrable, then f + g is integrable iff g is. See integrable_add_iff_integrable_right' for the same statement with fun x ↦ f x + g x instead of f + g.

Defined in

Mathlib.MeasureTheory.Function.L1Space.Integrable

Cited by

3 results in Mathlib

Foundations

Depth 208 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroup