This relation is known as the triangle inequality.
Assumptions:
TeX:
\left|a + b\right| \le \left|a\right| + \left|b\right|
a \in \mathbb{C} \,\mathbin{\operatorname{and}}\, b \in \mathbb{C}Definitions:
| Fungrim symbol | Notation | Short description |
|---|---|---|
| Abs | Absolute value | |
| CC | Complex numbers |
Source code for this entry:
Entry(ID("a6e081"),
Formula(LessEqual(Abs(Add(a, b)), Add(Abs(a), Abs(b)))),
Description("This relation is known as the triangle inequality."),
Variables(a, b),
Assumptions(And(Element(a, CC), Element(b, CC))))