cosh — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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