Tactics for measure theory #
Currently we have one domain-specific tactic for measure theory: measurability
.
This tactic is to a large extent a copy of the continuity
tactic by Reid Barton.
measurability
tactic #
Automatically solve goals of the form measurable f
, ae_measurable f μ
and measurable_set s
.
Mark lemmas with @[measurability]
to add them to the set of lemmas
used by measurability
. Note: to_additive
doesn't know yet how to
copy the attribute to the additive version.