Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-23 09:47 5ab7eb0f

View on Github →

feat(analysis/special_functions/trigonometric): continuity and differentiability of arctan (#4138) Added lemmas for continuity and differentiability of arctan, as well as various supporting limit lemmas.

Estimated changes

added theorem deriv_arctan
added theorem deriv_within_arctan
added theorem differentiable.arctan
added theorem has_deriv_at.arctan
added theorem real.arctan_mem_Ioo
added theorem real.continuous_arctan
added theorem real.deriv_arctan
modified theorem real.deriv_tan_of_mem_Ioo
modified theorem real.exists_cos_eq
modified theorem real.exists_cos_eq_zero
modified theorem real.exists_sin_eq
modified theorem real.range_cos
modified theorem real.range_sin
deleted theorem tendsto_at_top_div
deleted theorem tendsto_at_top_mul_left'
deleted theorem tendsto_at_top_mul_left
deleted theorem tendsto_at_top_mul_right'
deleted theorem tendsto_at_top_mul_right
deleted theorem tendsto_inv_at_top_zero'
deleted theorem tendsto_inv_at_top_zero
deleted theorem tendsto_inv_zero_at_top
added theorem tendsto_at_top_div
added theorem tendsto_mul_at_bot
added theorem tendsto_mul_at_top