Documentation

Mathlib.Tactic.Measurability

Measurability #

We define the measurability tactic using aesop.

source
def attrMeasurability :
Lean.ParserDescr

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

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

      fun_prop is a (usually more powerful) alternative to measurability if your goal does not involve MeasurableSet.

      Equations
        Instances For
          source
          def tacticMeasurability? :
          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
              Equations
                Instances For
                  source
                  def measurability!? :
                  Lean.ParserDescr
                  Equations
                    Instances For