Commit 2023-06-05 03:59 311c2413

View on Github →

feat: port Analysis.SpecialFunctions.Arsinh (#4674)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/SpecialFunctions/Arsinh.lean

added theorem ContDiff.arsinh

added theorem ContDiffAt.arsinh

added theorem ContDiffOn.arsinh

added theorem ContDiffWithinAt.arsinh

added theorem Continuous.arsinh

added theorem ContinuousOn.arsinh

added theorem Differentiable.arsinh

added theorem DifferentiableAt.arsinh

added theorem DifferentiableOn.arsinh

added theorem DifferentiableWithinAt.arsinh

added theorem Filter.Tendsto.arsinh

added theorem HasDerivAt.arsinh

added theorem HasDerivWithinAt.arsinh

added theorem HasFDerivAt.arsinh

added theorem HasFDerivWithinAt.arsinh

added theorem HasStrictDerivAt.arsinh

added theorem HasStrictFDerivAt.arsinh

added def Real.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

added theorem Real.arsinh_sinh

added theorem Real.arsinh_strictMono

added theorem Real.arsinh_surjective

added theorem Real.arsinh_zero

added theorem Real.contDiff_arsinh

added theorem Real.continuous_arsinh

added theorem Real.cosh_arsinh

added theorem Real.differentiable_arsinh

added theorem Real.exp_arsinh

added theorem Real.hasDerivAt_arsinh

added theorem Real.hasStrictDerivAt_arsinh

added def Real.sinhEquiv

added def Real.sinhHomeomorph

added def Real.sinhOrderIso

added theorem Real.sinh_arsinh

added theorem Real.sinh_bijective

added theorem Real.sinh_surjective