Def MeasurableSpace.countablePartition

Modification history

2026-07-24 07:15
Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean
chore: add missing `noncomputable` (#41446) …
Deleted MeasurableSpace.countablePartitionView on Github →
2024-03-13 15:40
Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean
feat: countable filtration in a countably generated measurable space (#10945) …
Added MeasurableSpace.countablePartitionView on Github →