Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-24 11:42 943b1294

View on Github →

feat(analysis/special_functions/trigonometric): sin, cos, sinh, and cosh are infinitely smooth (#5090)

Estimated changes

added theorem fderiv_ccos
added theorem fderiv_ccosh
added theorem fderiv_cos
added theorem fderiv_cosh
added theorem fderiv_csin
added theorem fderiv_csinh
added theorem fderiv_sin
added theorem fderiv_sinh
added theorem fderiv_within_ccos
added theorem fderiv_within_ccosh
added theorem fderiv_within_cos
added theorem fderiv_within_cosh
added theorem fderiv_within_csin
added theorem fderiv_within_csinh
added theorem fderiv_within_sin
added theorem fderiv_within_sinh
added theorem has_fderiv_at.ccos
added theorem has_fderiv_at.ccosh
added theorem has_fderiv_at.cos
added theorem has_fderiv_at.cosh
added theorem has_fderiv_at.csin
added theorem has_fderiv_at.csinh
added theorem has_fderiv_at.sin
added theorem has_fderiv_at.sinh
modified theorem measurable.ccos
modified theorem measurable.ccosh
modified theorem measurable.cos
modified theorem measurable.cosh
modified theorem measurable.csin
modified theorem measurable.csinh
modified theorem measurable.sin
modified theorem measurable.sinh
added theorem times_cont_diff.ccos
added theorem times_cont_diff.ccosh
added theorem times_cont_diff.cos
added theorem times_cont_diff.cosh
added theorem times_cont_diff.csin
added theorem times_cont_diff.csinh
added theorem times_cont_diff.sin
added theorem times_cont_diff.sinh
added theorem times_cont_diff_at.cos
added theorem times_cont_diff_at.sin
added theorem times_cont_diff_on.cos
added theorem times_cont_diff_on.sin