Fungrim entry: 920cc8

Symbol: Abs —

\left|z\right|

— Absolute value

Domain	Codomain
$z \in \mathbb{R}$	$\left\|z\right\| \in \left[0, \infty\right)$
$z \in \mathbb{C}$	$\left\|z\right\| \in \left[0, \infty\right)$
$z \in \left\{\infty, -\infty, {\tilde \infty}\right\}$	$\left\|z\right\| \in \left\{\infty\right\}$

Table data:

\left(P, Q\right)

such that

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

Definitions:

Fungrim symbol	Notation	Short description
`Abs`	$\left\|z\right\|$	Absolute value
`RR`	$\mathbb{R}$	Real numbers
`ClosedOpenInterval`	$\left[a, b\right)$	Closed-open interval
`Infinity`	$\infty$	Positive infinity
`CC`	$\mathbb{C}$	Complex numbers
`UnsignedInfinity`	${\tilde \infty}$	Unsigned infinity

Source code for this entry:

Entry(ID("920cc8"),
    SymbolDefinition(Abs, Abs(z), "Absolute value"),
    Table(TableRelation(Tuple(P, Q), Implies(P, Q)), TableHeadings(Description("Domain"), Description("Codomain")), List(Tuple(Element(z, RR), Element(Abs(z), ClosedOpenInterval(0, Infinity))), Tuple(Element(z, CC), Element(Abs(z), ClosedOpenInterval(0, Infinity))), Tuple(Element(z, Set(Infinity, Neg(Infinity), UnsignedInfinity)), Element(Abs(z), Set(Infinity))))))

Topics using this entry

Complex parts