Theorems · Theorem · measure theory

MeasureTheory.DominatedFinMeasAdditive.of_measure_le_smul

∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [inst : SeminormedAddCommGroup β]
  {T : Set α → β} {C : ℝ} {μ' : MeasureTheory.Measure α} {c : ENNReal},
  c ≠ ⊤ →
    μ ≤ c • μ' →
      MeasureTheory.DominatedFinMeasAdditive μ T C → 0 ≤ C → MeasureTheory.DominatedFinMeasAdditive μ' T (c.toReal * C)

Defined in

Mathlib.MeasureTheory.Integral.FinMeasAdditive

Cited by

0 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroup