Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-07 05:47 a32e2236

View on Github →

refactor(analysis/special_functions/trigonometric): redefine arcsin and arctan (#5300) Redefine arcsin and arctan using order_iso, and prove that both of them are infinitely smooth.

Estimated changes

added theorem fderiv_arctan
added theorem fderiv_within_arctan
added theorem has_fderiv_at.arctan
added theorem measurable.arctan
added theorem real.arccos_eq_pi
added theorem real.arccos_eq_zero
modified theorem real.arccos_inj
added theorem real.arccos_inj_on
modified theorem real.arcsin_eq_zero_iff
modified theorem real.arcsin_inj
modified theorem real.arcsin_le_pi_div_two
added theorem real.arcsin_lt_zero
added theorem real.arcsin_mem_Icc
modified theorem real.arcsin_neg_one
modified theorem real.arcsin_nonneg
modified theorem real.arcsin_nonpos
added theorem real.arcsin_of_one_le
modified theorem real.arcsin_pos
added theorem real.arcsin_proj_Icc
added theorem real.arcsin_sin'
added theorem real.arctan_eq_arcsin
added theorem real.continuous_arccos
added theorem real.continuous_arcsin
added theorem real.cos_arctan_pos
added theorem real.cos_sq_arctan
added theorem real.deriv_arccos
added theorem real.deriv_arcsin
added theorem real.deriv_arcsin_aux
added theorem real.image_tan_Ioo
added theorem real.inj_on_arcsin
added theorem real.inj_on_tan
added theorem real.maps_to_sin_Ioo
added theorem real.measurable_arccos
added theorem real.measurable_arcsin
added theorem real.measurable_arctan
added theorem real.monotone_arcsin
added theorem real.range_arcsin
added theorem real.sin_arcsin'
added theorem real.surj_on_tan
modified theorem real.tan_arctan
deleted def real.tan_homeomorph
added theorem times_cont_diff.arctan
added theorem subtype.coe_eq_iff