Theorem MeasureTheory.nonempty_of_isProbabilityMeasure

Modification history

2025-12-15 20:43
Mathlib/MeasureTheory/Measure/Typeclasses/Probability.lean
chore: smaller imports in `IonescuTulcea.traj` (#32895) …
Added MeasureTheory.nonempty_of_isProbabilityMeasureView on Github →