Fungrim home page

Fungrim entry: ce3a8e

Symbol: Atan2 atan2 ⁣(y,x)\operatorname{atan2}\!\left(y, x\right) Two-argument inverse tangent
The inverse tangent function atan2 ⁣(y,x)\operatorname{atan2}\!\left(y, x\right) (denoted by Atan2(y, x) in the Fungrim formula language) is a function of two variables. The following table lists conditions such that Atan2(y, x) is defined in Fungrim.
Domain Codomain
Numbers
yRandxRy \in \mathbb{R} \,\mathbin{\operatorname{and}}\, x \in \mathbb{R} atan2 ⁣(y,x)(π,π]\operatorname{atan2}\!\left(y, x\right) \in \left(-\pi, \pi\right]
Table data: (P,Q)\left(P, Q\right) such that (P)    (Q)\left(P\right) \implies \left(Q\right)
Definitions:
Fungrim symbol Notation Short description
Atan2atan2 ⁣(y,x)\operatorname{atan2}\!\left(y, x\right) Two-argument inverse tangent
RRR\mathbb{R} Real numbers
OpenClosedInterval(a,b]\left(a, b\right] Open-closed interval
ConstPiπ\pi The constant pi (3.14...)
Source code for this entry:
Entry(ID("ce3a8e"),
    SymbolDefinition(Atan2, Atan2(y, x), "Two-argument inverse tangent"),
    Description("The inverse tangent function", Atan2(y, x), "(denoted by", SourceForm(Atan2(y, x)), "in the Fungrim formula language)", "is a function of two variables.", "The following table lists conditions such that", SourceForm(Atan2(y, x)), "is defined in Fungrim."),
    Table(TableRelation(Tuple(P, Q), Implies(P, Q)), TableHeadings(Description("Domain"), Description("Codomain")), List(TableSection("Numbers"), Tuple(And(Element(y, RR), Element(x, RR)), Element(Atan2(y, x), OpenClosedInterval(Neg(ConstPi), ConstPi))))))

Topics using this entry

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

2019-06-18 07:49:59.356594 UTC