Theorem MeasureTheory.Measure.LebesgueDecomposition.iSup_monotone'

Modification history

2023-08-10 19:52

Mathlib/MeasureTheory/Decomposition/Lebesgue.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified MeasureTheory.Measure.LebesgueDecomposition.iSup_monotone'View on Github →

2023-06-07 04:25

Mathlib/MeasureTheory/Decomposition/Lebesgue.lean

feat: port MeasureTheory.Decomposition.Lebesgue (#4736)

Added MeasureTheory.Measure.LebesgueDecomposition.iSup_monotone'View on Github →