feat: port MeasureTheory.Measure.VectorMeasure (#4016)

Co-authored-by: Komyyy <pol_tta@outlook.jp>
leanprover-community · May 29, 2023 · a6e9434 · a6e9434
1 parent deff4e1
commit a6e9434
Show file tree

Hide file tree

Showing 2 changed files with 1,442 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1866,6 +1866,7 @@ import Mathlib.MeasureTheory.Measure.OuterMeasure
 import Mathlib.MeasureTheory.Measure.Regular
 import Mathlib.MeasureTheory.Measure.Stieltjes
 import Mathlib.MeasureTheory.Measure.Sub
+import Mathlib.MeasureTheory.Measure.VectorMeasure
 import Mathlib.MeasureTheory.PiSystem
 import Mathlib.MeasureTheory.Tactic
 import Mathlib.ModelTheory.Basic