Measurability

We define the measurability tactic using aesop.

def attrMeasurability : Lean.ParserDescr

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

Equations

• attrMeasurability = Lean.ParserDescr.node `attrMeasurability 1024 (Lean.ParserDescr.nonReservedSymbol "measurability" false)

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.

Equations

• One or more equations did not get rendered due to their size.

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

• One or more equations did not get rendered due to their size.

def measurability! : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def measurability!? : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.