sinh — Mathlib

English

The real hyperbolic sine is the real part of the complex hyperbolic sine on real inputs; i.e., for x ∈ ℝ, Real.sinh x = Re( Complex.sinh( Complex.ofReal x ) ).

Русский

Гиперболическая синус на вещественных входах равна вещественной части комплексной гиперболической синус: Real.sinh x = Re( Complex.sinh( Complex.ofReal x ) ).

LaTeX

$$$$ \operatorname{Real.sinh}(x) = \operatorname{Re}\bigl( \operatorname{sinh}(\operatorname{Complex.ofReal}(x)) \bigr). $$$$

Lean4

/-- The real hypebolic sine function, defined as the real part of the complex hyperbolic sine -/
@[pp_nodot]
nonrec def sinh (x : ℝ) : ℝ :=
  (sinh x).re

Похожие утверждения