# Fungrim entry: a2af66

$\operatorname{atan2}\!\left(y, x\right) = \mathop{\operatorname{solution*}\,}\limits_{\theta \in \left(-\pi, \pi\right]} \left[\left(x, y\right) = \left(r \cos(\theta), r \sin(\theta)\right)\; \text{ where } r = \sqrt{{x}^{2} + {y}^{2}}\right]$
Assumptions:$x \in \mathbb{R} \;\mathbin{\operatorname{and}}\; y \in \mathbb{R} \;\mathbin{\operatorname{and}}\; \left(x \ne 0 \;\mathbin{\operatorname{or}}\; y \ne 0\right)$
TeX:
\operatorname{atan2}\!\left(y, x\right) = \mathop{\operatorname{solution*}\,}\limits_{\theta \in \left(-\pi, \pi\right]} \left[\left(x, y\right) = \left(r \cos(\theta), r \sin(\theta)\right)\; \text{ where } r = \sqrt{{x}^{2} + {y}^{2}}\right]

x \in \mathbb{R} \;\mathbin{\operatorname{and}}\; y \in \mathbb{R} \;\mathbin{\operatorname{and}}\; \left(x \ne 0 \;\mathbin{\operatorname{or}}\; y \ne 0\right)
Definitions:
Fungrim symbol Notation Short description
Atan2$\operatorname{atan2}\!\left(y, x\right)$ Two-argument inverse tangent
UniqueSolution$\mathop{\operatorname{solution*}\,}\limits_{x \in S} Q(x)$ Unique solution
Cos$\cos(z)$ Cosine
Sin$\sin(z)$ Sine
Sqrt$\sqrt{z}$ Principal square root
Pow${a}^{b}$ Power
OpenClosedInterval$\left(a, b\right]$ Open-closed interval
Pi$\pi$ The constant pi (3.14...)
RR$\mathbb{R}$ Real numbers
Source code for this entry:
Entry(ID("a2af66"),
Formula(Equal(Atan2(y, x), UniqueSolution(Brackets(Where(Equal(Tuple(x, y), Tuple(Mul(r, Cos(theta)), Mul(r, Sin(theta)))), Equal(r, Sqrt(Add(Pow(x, 2), Pow(y, 2)))))), ForElement(theta, OpenClosedInterval(Neg(Pi), Pi))))),
Variables(x, y),
Assumptions(And(Element(x, RR), Element(y, RR), Or(NotEqual(x, 0), NotEqual(y, 0)))))

## Topics using this entry

Copyright (C) Fredrik Johansson and contributors. Fungrim is provided under the MIT license. The source code is on GitHub.

2020-08-27 09:56:25.682319 UTC