# 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

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

2021-03-15 19:12:00.328586 UTC