Def MeasureTheory.Measure.InnerRegular

Modification history

2023-11-08 23:58

Mathlib/MeasureTheory/Measure/Regular.lean

feat: new class `InnerRegular` of measures (#8251) …

Deleted MeasureTheory.Measure.InnerRegular View on Github →

2023-05-21 16:29

Mathlib/MeasureTheory/Measure/Regular.lean

feat: port MeasureTheory.Measure.Regular (#4101)

Added MeasureTheory.Measure.InnerRegular View on Github →