Skip to content

Commit b1a047a

Browse files
KomyyyMonadMaverickParcly-Taxel
committed
feat: port MeasureTheory.Measure.NullMeasurable (#3349)
Co-authored-by: MonadMaverick <MonadMaverick@pm.me> Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
1 parent 3cef175 commit b1a047a

File tree

2 files changed

+521
-0
lines changed

2 files changed

+521
-0
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1533,6 +1533,7 @@ import Mathlib.MeasureTheory.MeasurableSpace
15331533
import Mathlib.MeasureTheory.MeasurableSpaceDef
15341534
import Mathlib.MeasureTheory.Measure.AEDisjoint
15351535
import Mathlib.MeasureTheory.Measure.MeasureSpaceDef
1536+
import Mathlib.MeasureTheory.Measure.NullMeasurable
15361537
import Mathlib.MeasureTheory.Measure.OuterMeasure
15371538
import Mathlib.MeasureTheory.PiSystem
15381539
import Mathlib.ModelTheory.Basic

0 commit comments

Comments
 (0)