Commit 2023-05-21 21:51 d15ff064

View on Github →

feat: port MeasureTheory.Function.SpecialFunctions.Basic (#4175)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Function/SpecialFunctions/Basic.lean

added theorem Complex.measurable_arg

added theorem Complex.measurable_cos

added theorem Complex.measurable_cosh

added theorem Complex.measurable_exp

added theorem Complex.measurable_im

added theorem Complex.measurable_log

added theorem Complex.measurable_of_real

added theorem Complex.measurable_re

added theorem Complex.measurable_sin

added theorem Complex.measurable_sinh

added theorem Measurable.carg

added theorem Measurable.ccos

added theorem Measurable.ccosh

added theorem Measurable.cexp

added theorem Measurable.clog

added theorem Measurable.cos

added theorem Measurable.cosh

added theorem Measurable.csin

added theorem Measurable.csinh

added theorem Measurable.exp

added theorem Measurable.log

added theorem Measurable.sin

added theorem Measurable.sinh

added theorem Measurable.sqrt

added theorem Real.measurable_arccos

added theorem Real.measurable_arcsin

added theorem Real.measurable_cos

added theorem Real.measurable_cosh

added theorem Real.measurable_exp

added theorem Real.measurable_log

added theorem Real.measurable_sin

added theorem Real.measurable_sinh