Assumptions:
TeX:
\operatorname{atan}\!\left(x\right) \ge \frac{x}{\sqrt{1 + {x}^{2}}}
x \in \left[0, \infty\right)Definitions:
| Fungrim symbol | Notation | Short description |
|---|---|---|
| Atan | Inverse tangent | |
| Sqrt | Principal square root | |
| Pow | Power | |
| ClosedOpenInterval | Closed-open interval | |
| Infinity | Positive infinity |
Source code for this entry:
Entry(ID("b0a4e9"),
Formula(GreaterEqual(Atan(x), Div(x, Sqrt(Add(1, Pow(x, 2)))))),
Variables(x),
Assumptions(Element(x, ClosedOpenInterval(0, Infinity))))