Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-09 01:12 9e320a22

View on Github →

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

Estimated changes

modified theorem complex.measurable_arg
modified theorem complex.measurable_cos
modified theorem complex.measurable_cosh
modified theorem complex.measurable_exp
modified theorem complex.measurable_im
modified theorem complex.measurable_log
modified theorem complex.measurable_of_real
modified theorem complex.measurable_re
modified theorem complex.measurable_sin
modified theorem complex.measurable_sinh
modified theorem measurable.arctan
modified theorem measurable.carg
modified theorem measurable.ccos
modified theorem measurable.ccosh
modified theorem measurable.cexp
modified theorem measurable.clog
modified theorem measurable.cos
modified theorem measurable.cosh
modified theorem measurable.csin
modified theorem measurable.csinh
modified theorem measurable.exp
modified theorem measurable.log
modified theorem measurable.sin
modified theorem measurable.sinh
modified theorem measurable.sqrt
modified theorem real.measurable_arccos
modified theorem real.measurable_arcsin
modified theorem real.measurable_arctan
modified theorem real.measurable_cos
modified theorem real.measurable_cosh
modified theorem real.measurable_exp
modified theorem real.measurable_log
modified theorem real.measurable_sin
modified theorem real.measurable_sinh