Commit 2021-06-09 20:42 d9b91f3b
View on Github →feat(measure_theory/tactic): add measurability tactic (#7756)
Add a measurability tactic defined in the file measure_theory/tactic.lean
, which is heavily inspired from the continuity tactic. It proves goals of the form measurable f
, ae_measurable f µ
and measurable_set s
. Some tests are provided in tests/measurability.lean
and the tactic was used to replace a few lines in integration.lean
and mean_inequalities.lean
.