Theorem Measurable.measure_of_isPiSystem_of_isProbabilityMeasure

Modification history

2024-12-12 18:01
Mathlib/MeasureTheory/Measure/GiryMonad.lean
feat(GiryMonad): add `Measurable.measure_of_isPiSystem` (#19908) …
Added Measurable.measure_of_isPiSystem_of_isProbabilityMeasureView on Github →