Arctangent

Definition

The arctangent is the function $\arctan \colon \mathbb{R} \to (-\pi/2, \pi/2)$ such that, for each real $x$, $\arctan x$ is the unique $y \in (-\pi/2, \pi/2)$ with $\tan y = x$.

Remarks

The tangent is strictly increasing and continuous on $(-\pi/2, \pi/2)$, with range $\mathbb{R}$. So $\arctan$ is well defined and continuous. For example, $\arctan 0 = 0$ and $\arctan 1 = \pi/4$. Also $\arctan x \to \pi/2$ as $x \to \infty$, and $\arctan x \to -\pi/2$ as $x \to -\infty$. Mathlib defines it as Real.arctan.

Explanations

L1 human

The arctangent of $x$ is the angle between $-\pi/2$ and $\pi/2$ whose tangent is $x$. It is the angle of a line with slope $x$.