Measurability

We define the measurability tactic using aesop.

def measurability : Lean.ParserDescr

The measurability attribute used to tag measurability statements for the measurability tactic.

Note that measurability uses fun_prop for solving measurability of functions, so statements about Measurable, AEMeasurable, StronglyMeasurable and AEStronglyMeasurable should be tagged with fun_prop rather that measurability. The measurability attribute is equivalent to fun_prop in these cases for backward compatibility with the earlier implementation.

def Mathlib.Tactic.measurability : Lean.ParserDescr

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.

Note that measurability uses fun_prop for solving measurability of functions, so statements about Measurable, AEMeasurable, StronglyMeasurable and AEStronglyMeasurable should be tagged with fun_prop rather that measurability. The measurability attribute is equivalent to fun_prop in these cases for backward compatibility with the earlier implementation.

def Mathlib.Tactic.measurability? : Lean.ParserDescr

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.

def measurability! : Lean.ParserDescr

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.

Note that measurability uses fun_prop for solving measurability of functions, so statements about Measurable, AEMeasurable, StronglyMeasurable and AEStronglyMeasurable should be tagged with fun_prop rather that measurability. The measurability attribute is equivalent to fun_prop in these cases for backward compatibility with the earlier implementation.

def measurability!? : Lean.ParserDescr

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.