ThmDex – An index of mathematical definitions, results, and conjectures.
 ▼ Set of symbols ▼ Alphabet ▼ Deduction system ▼ Theory ▼ Zermelo-Fraenkel set theory ▼ Set ▼ Binary cartesian set product ▼ Binary relation ▼ Map ▼ Operation ▼ N-operation ▼ Binary operation ▼ Enclosed binary operation ▼ Groupoid ▼ Semigroup ▼ Standard N-operation ▼ Indexed sum ▼ Series ▼ Power series ▼ Convergent power series ▼ Natural complex exponential function ▼ Standard natural complex exponential function ▼ Standard natural complex hyperbolic cosine function
Definition D1933
Standard natural hyperbolic cosine function

Let $x \mapsto e^x$ be the D1932: Standard natural real exponential function.
The standard natural hyperbolic cosine function is the D4364: Real function $$\cosh : \mathbb{R} \to \mathbb{R}, \quad \cosh(x) = \frac{1}{2} (e^x + e^{-x})$$

Let $\exp$ be the D1932: Standard natural real exponential function.
The standard natural hyperbolic cosine function is the D4364: Real function $$\cosh : \mathbb{R} \to \mathbb{R}, \quad \cosh(x) = \frac{1}{2} (\exp(x) + \exp(-x))$$