Theorems · Definition · measure theory
MeasureTheory.FiniteMeasure
(Ω : Type u_2) → [MeasurableSpace Ω] → Type u_2
Finite measures are defined as the subtype of measures that have the property of being finite measures (i.e., their total mass is finite).
- Cited by
- 150 results in Mathlib
- Foundations
- Depth 3 from the axioms, rests on 5 definitions · uses no axioms
- Assumes
- MeasurableSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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.Measureproof · cited by 10,939
- MeasureTheory.IsFiniteMeasureproof · cited by 1,078
Cited by164
Results whose statement or proof uses this declaration.
- MeasureTheory.FiniteMeasure.toMeasurestatement · cited by 87
- MeasureTheory.FiniteMeasure.massstatement and proof · cited by 46
- MeasureTheory.FiniteMeasure.testAgainstNNstatement and proof · cited by 27
- MeasureTheory.ProbabilityMeasure.toFiniteMeasurestatement · cited by 26
- MeasureTheory.FiniteMeasure.mapstatement and proof · cited by 16
- MeasureTheory.FiniteMeasure.normalizestatement and proof · cited by 15
- MeasureTheory.FiniteMeasure.eq_of_forall_toMeasure_apply_eqstatement and proof · cited by 13
- MeasureTheory.FiniteMeasure.ennreal_coeFn_eq_coeFn_toMeasurestatement and proof · cited by 11
- MeasureTheory.FiniteMeasure.prodstatement and proof · cited by 11
- MeasureTheory.FiniteMeasure.restrictstatement and proof · cited by 10
- MeasureTheory.FiniteMeasure.toWeakDualBCNNstatement and proof · cited by 8
- MeasureTheory.FiniteMeasure.mass_nonzero_iffstatement and proof · cited by 6