Theorems · Theorem · measure theory

MeasureTheory.LocallyIntegrable.add

∀ {X : Type u_1} {ε'' : Type u_5} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace ε''] [inst_3 : ESeminormedAddMonoid ε''] {μ : MeasureTheory.Measure X} [ContinuousAdd ε'']
  {f g : X → ε''},
  MeasureTheory.LocallyIntegrable f μ → MeasureTheory.LocallyIntegrable g μ → MeasureTheory.LocallyIntegrable (f + g) μ

Defined in

Mathlib.MeasureTheory.Function.LocallyIntegrable

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceTopologicalSpaceESeminormedAddMonoidContinuousAdd