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
Convergent basic real power series
Definition D1927
Standard real cosine function
Formulation 0
The standard real cosine function is the D4364: Real function \begin{equation} \mathbb{R} \to [-1, 1], \quad x \mapsto \lim_{N \to \infty} \sum_{n = 0}^N (-1)^n \frac{x^{2n}}{(2n)!} \end{equation}
Formulation 1
The standard real cosine function is the D4364: Real function \begin{equation} \mathbb{R} \to [-1, 1], \quad x \mapsto \sum_{n = 0}^{\infty} (-1)^n \frac{x^{2n}}{(2n)!} \end{equation}
Formulation 2
The standard real cosine function is the D4364: Real function \begin{equation} \mathbb{R} \to [-1, 1], \quad x \mapsto 1 - \frac{x^2}{2!} + \frac{x^4}{4!} - \frac{x^6}{6!} + \frac{x^8}{8!} - \dots \end{equation}
Children
Weierstrass function
Conventions
Convention 0 (Notation for standard basic real cosine function)
The notation used for the D1927: Standard real cosine function is $x \mapsto \cos(x)$.