mathlib3
9e320a22 - chore(measure_theory/special_functions): add measurability attributes (#8570)

Commit

4 years ago

chore(measure_theory/special_functions): add measurability attributes (#8570) That attribute makes the `measurability` tactic aware of those lemmas.

Author

RemyDegenne

Parents