Fungrim entry: b7d740

Symbol: Arg —

\arg(z)

— Complex argument

Domain	Codomain
$z \in \mathbb{R}$	$\arg(z) \in \left\{0, \pi\right\}$
$z \in \mathbb{C}$	$\arg(z) \in \left(-\pi, \pi\right]$
$z \in \left\{\infty\right\}$	$\arg(z) \in \left\{0\right\}$
$z \in \left\{-\infty\right\}$	$\arg(z) \in \left\{\pi\right\}$

Table data:

\left(P, Q\right)

such that

\left(P\right) \;\implies\; \left(Q\right)

Definitions:

Fungrim symbol	Notation	Short description
`Arg`	$\arg(z)$	Complex argument
`RR`	$\mathbb{R}$	Real numbers
`Pi`	$\pi$	The constant pi (3.14...)
`CC`	$\mathbb{C}$	Complex numbers
`OpenClosedInterval`	$\left(a, b\right]$	Open-closed interval
`Infinity`	$\infty$	Positive infinity

Source code for this entry:

Entry(ID("b7d740"),
    SymbolDefinition(Arg, Arg(z), "Complex argument"),
    Table(TableRelation(Tuple(P, Q), Implies(P, Q)), TableHeadings(Description("Domain"), Description("Codomain")), List(Tuple(Element(z, RR), Element(Arg(z), Set(0, Pi))), Tuple(Element(z, CC), Element(Arg(z), OpenClosedInterval(Neg(Pi), Pi))), Tuple(Element(z, Set(Infinity)), Element(Arg(z), Set(0))), Tuple(Element(z, Set(Neg(Infinity))), Element(Arg(z), Set(Pi))))))

Topics using this entry

Complex parts