Arcsine

Definition

The arcsine is the function $\arcsin \colon [-1, 1] \to [-\pi/2, \pi/2]$ such that, for each $x \in [-1, 1]$, $\arcsin x$ is the unique $y \in [-\pi/2, \pi/2]$ with $\sin y = x$.

Remarks

The sine is strictly increasing and continuous on $[-\pi/2, \pi/2]$, with range $[-1, 1]$. So $\arcsin$ is well defined and continuous. For example, $\arcsin 0 = 0$, $\arcsin 1 = \pi/2$, and $\arcsin \frac{1}{2} = \pi/6$. The function is odd and strictly increasing. Mathlib defines Real.arcsin on all of $\mathbb{R}$, constant outside $[-1, 1]$.

Explanations

L1 human

The arcsine of $x$ is the angle between $-\pi/2$ and $\pi/2$ whose sine is $x$.