Documentation

Mathlib.Tactic.Measurability

Measurability #

We define the measurability tactic using aesop.

source
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.

Equations
Instances For
    source
    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.

    Equations
    Instances For
      source
      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.

      Equations
      Instances For
        source
        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.

        Equations
        Instances For
          source
          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.

          Equations
          Instances For