Theorems · Theorem · measure theory

MeasureTheory.isFiniteMeasure_of_le

∀ {α : Type u_1} {m0 : MeasurableSpace α} {ν : MeasureTheory.Measure α} (μ : MeasureTheory.Measure α)
  [MeasureTheory.IsFiniteMeasure μ], ν ≤ μ → MeasureTheory.IsFiniteMeasure ν

Defined in: Mathlib.MeasureTheory.Measure.Typeclasses.Finite
Cited by: 4 results in Mathlib
Foundations: Depth 173 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasureTheory.IsFiniteMeasure

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites6

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

MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
Set.univproof · cited by 3,945
MeasureTheory.IsFiniteMeasurestatement and proof · cited by 1,078
LE.le.trans_ltproof · cited by 795
MeasureTheory.measure_lt_topproof · cited by 39

Cited by4

Results whose statement or proof uses this declaration.

MeasureTheory.AEContinuous.hasBoxIntegralproof · cited by 1
MeasureTheory.Measure.haveLebesgueDecomposition_of_finiteMeasureproof · cited by 0
MeasureTheory.Measure.IsFiniteMeasure.IicSndproof · cited by 0
MeasureTheory.VectorMeasure.exists_extension_of_isSetSemiring_of_le_measureproof · cited by 0