Commit 2023-05-30 06:20 e28e13ff

View on Github →

feat: port MeasureTheory.Category.Meas (#4487)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Category/MeasCat.lean

added def Borel

added def MeasCat.Giry

added def MeasCat.Integral

added def MeasCat.Measure

added theorem MeasCat.coe_of

added def MeasCat.of

added def MeasCat