Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-16 02:00 0053e3c5

View on Github →

feat(analysis/special_functions/arsinh): add lemmas, review API (#14668)

Estimated changes

Modified src/analysis/calculus/cont_diff.lean

added theorem homeomorph.cont_diff_symm

added theorem homeomorph.cont_diff_symm_deriv

Modified src/analysis/special_functions/arsinh.lean

added theorem cont_diff.arsinh

added theorem cont_diff_at.arsinh

added theorem cont_diff_on.arsinh

added theorem cont_diff_within_at.arsinh

added theorem continuous.arsinh

added theorem continuous_at.arsinh

added theorem continuous_on.arsinh

added theorem continuous_within_at.arsinh

added theorem differentiable.arsinh

added theorem differentiable_at.arsinh

added theorem differentiable_on.arsinh

added theorem differentiable_within_at.arsinh

added theorem filter.tendsto.arsinh

added theorem has_deriv_at.arsinh

added theorem has_deriv_within_at.arsinh

added theorem has_fderiv_at.arsinh

added theorem has_fderiv_within_at.arsinh

added theorem has_strict_deriv_at.arsinh

added theorem has_strict_fderiv_at.arsinh

added theorem real.arsinh_bijective

added theorem real.arsinh_eq_zero_iff

added theorem real.arsinh_inj

added theorem real.arsinh_injective

added theorem real.arsinh_le_arsinh

added theorem real.arsinh_lt_arsinh

added theorem real.arsinh_neg

added theorem real.arsinh_neg_iff

added theorem real.arsinh_nonneg_iff

added theorem real.arsinh_nonpos_iff

added theorem real.arsinh_pos_iff

modified theorem real.arsinh_sinh

added theorem real.arsinh_strict_mono

added theorem real.arsinh_surjective

added theorem real.arsinh_zero

added theorem real.cont_diff_arsinh

added theorem real.continuous_arsinh

added theorem real.cosh_arsinh

added theorem real.differentiable_arsinh

added theorem real.exp_arsinh

added theorem real.has_deriv_at_arsinh

added theorem real.has_strict_deriv_at_arsinh

modified theorem real.sinh_arsinh

modified theorem real.sinh_bijective

added def real.sinh_equiv

added def real.sinh_homeomorph

added def real.sinh_order_iso

modified theorem real.sinh_surjective

deleted theorem real.sqrt_one_add_sinh_sq