Measurability #
We define the measurability
tactic using aesop
.
The measurability
attribute used to tag continuity statements for the measurability
tactic.
Instances For
The tactic measurability
solves goals of the form Measurable f
, AEMeasurable f
,
StronglyMeasurable f
, AEStronglyMeasurable f μ
, or MeasurableSet s
by applying lemmas tagged
with the measurability
user attribute.
Instances For
The tactic measurability?
solves goals of the form Measurable f
, AEMeasurable f
,
StronglyMeasurable f
, AEStronglyMeasurable f μ
, or MeasurableSet s
by applying lemmas tagged
with the measurability
user attribute, and suggests a faster proof script that can be substituted
for the tactic call in case of success.