Theorem Measurable.measure_of_isPiSystem

Modification history

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