Def MeasurableSpace.DynkinSystem.toMeasurableSpace

Modification history

2023-02-11 09:36

Mathlib/MeasureTheory/PiSystem.lean

feat: port MeasureTheory.PiSystem (#2160)

Added MeasurableSpace.DynkinSystem.toMeasurableSpace View on Github →