Assumptions:
TeX:
\left|\operatorname{atan}(x)\right| < \frac{\pi}{2}
x \in \mathbb{R}Definitions:
| Fungrim symbol | Notation | Short description |
|---|---|---|
| Abs | Absolute value | |
| Atan | Inverse tangent | |
| Pi | The constant pi (3.14...) | |
| RR | Real numbers |
Source code for this entry:
Entry(ID("e7a9b1"),
Formula(Less(Abs(Atan(x)), Div(Pi, 2))),
Variables(x),
Assumptions(Element(x, RR)))