Fungrim entry: 22fb4a

\operatorname{atan2}\!\left(y, x\right) = \begin{cases} 0, & x = y = 0\\\operatorname{atan}\!\left(\frac{y}{x}\right), & x > 0\\\left(\frac{\pi}{2}\right) \operatorname{sgn}(y) - \operatorname{atan}\!\left(\frac{x}{y}\right), & y \ne 0\\\pi, & y = 0 \;\mathbin{\operatorname{and}}\; x < 0\\ \end{cases}

Assumptions:

x \in \mathbb{R} \;\mathbin{\operatorname{and}}\; y \in \mathbb{R}

TeX:

\operatorname{atan2}\!\left(y, x\right) = \begin{cases} 0, & x = y = 0\\\operatorname{atan}\!\left(\frac{y}{x}\right), & x > 0\\\left(\frac{\pi}{2}\right) \operatorname{sgn}(y) - \operatorname{atan}\!\left(\frac{x}{y}\right), & y \ne 0\\\pi, & y = 0 \;\mathbin{\operatorname{and}}\; x < 0\\ \end{cases}

x \in \mathbb{R} \;\mathbin{\operatorname{and}}\; y \in \mathbb{R}

Definitions:

Fungrim symbol	Notation	Short description
`Atan2`	$\operatorname{atan2}\!\left(y, x\right)$	Two-argument inverse tangent
`Atan`	$\operatorname{atan}(z)$	Inverse tangent
`Pi`	$\pi$	The constant pi (3.14...)
`Sign`	$\operatorname{sgn}(z)$	Sign function
`RR`	$\mathbb{R}$	Real numbers

Source code for this entry:

Entry(ID("22fb4a"),
    Formula(Equal(Atan2(y, x), Cases(Tuple(0, Equal(x, y, 0)), Tuple(Atan(Div(y, x)), Greater(x, 0)), Tuple(Sub(Mul(Parentheses(Div(Pi, 2)), Sign(y)), Atan(Div(x, y))), NotEqual(y, 0)), Tuple(Pi, And(Equal(y, 0), Less(x, 0)))))),
    Variables(x, y),
    Assumptions(And(Element(x, RR), Element(y, RR))))

Topics using this entry

Inverse tangent