# Measurability #

We define the `measurability`

tactic using `aesop`

.

The `measurability`

attribute used to tag measurability statements for the `measurability`

tactic.

## Equations

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

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

## Equations

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

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

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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