Theorems · Definition · measure theory
MeasureTheory.FiniteMeasure.mass
{Ω : Type u_1} → [inst : MeasurableSpace Ω] → MeasureTheory.FiniteMeasure Ω → NNRealThe (total) mass of a finite measure μ is μ univ, i.e., the cast to NNReal of
(μ : measure Ω) univ.
- Cited by
- 46 results in Mathlib
- Foundations
- Depth 177 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- MeasurableSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- MeasurableSpacestatement and proof · cited by 13,106
- NNRealstatement · cited by 4,310
- Set.univproof · cited by 3,945
- MeasureTheory.FiniteMeasurestatement and proof · cited by 150
Cited by47
Results whose statement or proof uses this declaration.
- MeasureTheory.FiniteMeasure.normalizeproof · cited by 15
- MeasureTheory.FiniteMeasure.mass_nonzero_iffstatement · cited by 6
- MeasureTheory.FiniteMeasure.mass_zero_iffstatement and proof · cited by 5
- MeasureTheory.ProbabilityMeasure.mass_toFiniteMeasurestatement · cited by 5
- MeasureTheory.FiniteMeasure.ennreal_massstatement · cited by 4
- isCompact_setOfPred_finiteMeasure_le_of_compactSpacestatement and proof · cited by 3
- MeasureTheory.FiniteMeasure.continuous_massstatement · cited by 3
- Filter.Tendsto.massstatement · cited by 3
- isCompact_setOfPred_finiteMeasure_le_of_isCompactstatement and proof · cited by 2
- isCompact_setOfPred_finiteMeasure_mass_eq_compl_isCompact_lestatement and proof · cited by 2
- isCompact_setOfPred_finiteMeasure_mass_le_compl_isCompact_lestatement and proof · cited by 2
- MeasureTheory.FiniteMeasure.tendsto_zero_testAgainstNN_of_tendsto_zero_massstatement and proof · cited by 2