Theorems · Theorem · measure theory

MeasureTheory.DominatedFinMeasAdditive.add_measure_right

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

Defined in

Mathlib.MeasureTheory.Integral.FinMeasAdditive

Cited by

2 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroup