Documentation

Mathlib.Tactic.Measurability

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.

      Instances For