Def MeasurableEquiv.piFinSuccAboveEquiv

Modification history

2023-12-13 23:06
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
chore: replace `piFinSuccAboveEquiv` with `piFinSuccAbove` (#9030) …
Deleted MeasurableEquiv.piFinSuccAboveEquivView on Github →
2023-08-10 19:52
Mathlib/MeasureTheory/MeasurableSpace.lean
chore: banish `Type _` and `Sort _` (#6499) …
Modified MeasurableEquiv.piFinSuccAboveEquivView on Github →
2023-02-11 07:44
Mathlib/MeasureTheory/MeasurableSpace.lean
feat: port MeasureTheory.MeasurableSpace (#2174)
Added MeasurableEquiv.piFinSuccAboveEquivView on Github →