Commit 2023-05-08 10:01 3d31c9ec

View on Github →

feat: port MeasureTheory.Tactic (#3816)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/MeasurableSpace.lean

Modified Mathlib/MeasureTheory/MeasurableSpaceDef.lean

modified theorem MeasurableSpace.measurableSet_top

Modified Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

added theorem Measurable.comp_aemeasurable'

Created Mathlib/MeasureTheory/Tactic.lean

Modified Mathlib/Tactic.lean

Created Mathlib/Tactic/Measurability.lean

Created Mathlib/Tactic/Measurability/Init.lean

Created test/measurability.lean