Theorems · Theorem · real analysis
Real.sinh_arsinh
∀ (x : ℝ), Real.sinh (Real.arsinh x) = x
arsinh is the right inverse of sinh.
- Defined in
- Mathlib.Analysis.SpecialFunctions.Arsinh
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 174 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- Real.expproof · cited by 871
- Real.sqrtproof · cited by 545
- sub_neg_eq_addproof · cited by 264
- Real.sinhstatement · cited by 142
- Real.arsinhstatement and proof · cited by 55
- neg_sqproof · cited by 31
- add_sub_add_right_eq_subproof · cited by 29
- add_self_div_twoproof · cited by 18
- Real.sinh_eqproof · cited by 5
- Real.exp_arsinhproof · cited by 2
- Real.arsinh_negproof · cited by 1
Cited by9
Results whose statement or proof uses this declaration.
- UpperHalfPlane.sinh_half_distproof · cited by 6
- Real.sinhEquivproof · cited by 5
- Real.cosh_arsinhproof · cited by 2
- Real.arsinh_nonneg_iffproof · cited by 1
- Real.arsinh_nonpos_iffproof · cited by 1
- UpperHalfPlane.cosh_distproof · cited by 1
- Real.sinh_surjectiveproof · cited by 1
- Real.tanh_arsinhproof · cited by 0
- Real.arsinh_sinhproof · cited by 0