feat: port MeasureTheory.Measure.MeasureSpaceDef (#3325)

Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Co-authored-by: Komyyy <pol_tta@outlook.jp>
leanprover-community · May 4, 2023 · 8e9ff28 · 8e9ff28
1 parent 96a2d91
commit 8e9ff28
Show file tree

Hide file tree

Showing 2 changed files with 729 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1526,6 +1526,7 @@ import Mathlib.Mathport.Syntax
 import Mathlib.MeasureTheory.CardMeasurableSpace
 import Mathlib.MeasureTheory.MeasurableSpace
 import Mathlib.MeasureTheory.MeasurableSpaceDef
+import Mathlib.MeasureTheory.Measure.MeasureSpaceDef
 import Mathlib.MeasureTheory.Measure.OuterMeasure
 import Mathlib.MeasureTheory.PiSystem
 import Mathlib.ModelTheory.Basic