Theorems · Definition · measure theory
MeasureTheory.FiniteMeasure.toMeasure
{Ω : Type u_1} → [inst : MeasurableSpace Ω] → MeasureTheory.FiniteMeasure Ω → MeasureTheory.Measure ΩCoercion from MeasureTheory.FiniteMeasure Ω to MeasureTheory.Measure Ω.
- Cited by
- 87 results in Mathlib
- Foundations
- Depth 4 from the axioms · 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.Measurestatement · cited by 10,939
- MeasureTheory.FiniteMeasurestatement · cited by 150
Cited by95
Results whose statement or proof uses this declaration.
- MeasureTheory.FiniteMeasure.testAgainstNNproof · cited by 27
- MeasureTheory.FiniteMeasure.mapproof · cited by 16
- MeasureTheory.FiniteMeasure.normalizeproof · 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.prodproof · cited by 11
- MeasureTheory.FiniteMeasure.restrictproof · cited by 10
- MeasureTheory.FiniteMeasure.testAgainstNN_coe_eqstatement and proof · cited by 5
- MeasureTheory.FiniteMeasure.apply_monoproof · cited by 5
- MeasureTheory.FiniteMeasure.comapproof · cited by 5
- MeasureTheory.FiniteMeasure.tendsto_iff_forall_lintegral_tendstostatement and proof · cited by 5
- MeasureTheory.FiniteMeasure.ennreal_massstatement · cited by 4