Theorems · Theorem · measure theory

MeasureTheory.DominatedFinMeasAdditive.of_measure_le

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

Defined in: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Cited by: 4 results in Mathlib
Foundations: Depth 174 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: SeminormedAddCommGroup

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites17

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
Setstatement and proof · cited by 53,352
Realstatement and proof · cited by 25,697
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
Top.topproof · cited by 9,680
MeasurableSetproof · cited by 3,075
SeminormedAddCommGroupstatement and proof · cited by 2,671
LT.lt.neproof · cited by 872
LE.le.trans_ltproof · cited by 795
mul_le_mul_of_nonneg_leftproof · cited by 361
Eq.trans_leproof · cited by 155

Cited by4

Results whose statement or proof uses this declaration.

MeasureTheory.setToFun_add_left''proof · cited by 3
MeasureTheory.DominatedFinMeasAdditive.add_measure_rightproof · cited by 2
MeasureTheory.DominatedFinMeasAdditive.add_measure_leftproof · cited by 2
MeasureTheory.DominatedFinMeasAdditive.of_measure_le_smulproof · cited by 0