Theorems · Definition · measure theory
MeasureTheory.ProbabilityMeasure.toMeasure
{Ω : Type u_1} → [inst : MeasurableSpace Ω] → MeasureTheory.ProbabilityMeasure Ω → MeasureTheory.Measure ΩCoercion from MeasureTheory.ProbabilityMeasure Ω to MeasureTheory.Measure Ω.
- Cited by
- 78 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.ProbabilityMeasurestatement · cited by 127
Cited by82
Results whose statement or proof uses this declaration.
- MeasureTheory.ProbabilityMeasure.toFiniteMeasureproof · cited by 26
- MeasureTheory.ProbabilityMeasure.mapstatement and proof · cited by 12
- MeasureTheory.ProbabilityMeasure.prodproof · cited by 9
- MeasureTheory.ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasurestatement and proof · cited by 8
- MeasureTheory.ProbabilityMeasure.measureReal_eq_coe_coeFnstatement and proof · cited by 4
- MeasureTheory.ProbabilityMeasure.eq_of_forall_toMeasure_apply_eqstatement and proof · cited by 3
- MeasureTheory.ProbabilityMeasure.le_liminf_measure_open_of_tendstostatement · cited by 3
- MeasureTheory.ProbabilityMeasure.piproof · cited by 3
- MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_lintegral_tendstostatement and proof · cited by 3
- MeasureTheory.tendsto_of_forall_isOpen_le_liminf_nat'statement and proof · cited by 2
- MeasureTheory.ProbabilityMeasure.continuous_iff_forall_continuous_integralstatement and proof · cited by 2