Arccosine

Definition

The arccosine is the function $\arccos \colon [-1, 1] \to [0, \pi]$ such that, for each $x \in [-1, 1]$, $\arccos x$ is the unique $y \in [0, \pi]$ with $\cos y = x$.

Remarks

The cosine is strictly decreasing and continuous on $[0, \pi]$, with range $[-1, 1]$. So $\arccos$ is well defined and continuous. For all $x \in [-1, 1]$, $\arccos x = \frac{\pi}{2} - \arcsin x$. For example, $\arccos 1 = 0$ and $\arccos(-1) = \pi$. Mathlib defines Real.arccos by the identity above.

Explanations

L1 human

The arccosine of $x$ is the angle between $0$ and $\pi$ whose cosine is $x$.