Theorems · Theorem · measure theory

MeasureTheory.DominatedFinMeasAdditive.add

∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [inst : SeminormedAddCommGroup β]
  {T T' : Set α → β} {C C' : ℝ},
  MeasureTheory.DominatedFinMeasAdditive μ T C →
    MeasureTheory.DominatedFinMeasAdditive μ T' C' → MeasureTheory.DominatedFinMeasAdditive μ (T + T') (C + C')

Defined in

Mathlib.MeasureTheory.Integral.FinMeasAdditive

Cited by

3 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroup