Assumptions:
TeX:
\log(x) \le x - 1 x \in \left(0, \infty\right)
Definitions:
| Fungrim symbol | Notation | Short description |
|---|---|---|
| Log | Natural logarithm | |
| OpenInterval | Open interval | |
| Infinity | Positive infinity |
Source code for this entry:
Entry(ID("4986ed"),
Formula(LessEqual(Log(x), Sub(x, 1))),
Variables(x),
Assumptions(Element(x, OpenInterval(0, Infinity))))