Assumptions:
TeX:
W\!\left(x \log(x)\right) = \log(x)
x \in \left[\frac{1}{e}, \infty\right)Definitions:
| Fungrim symbol | Notation | Short description |
|---|---|---|
| LambertW | Lambert W-function | |
| Log | Natural logarithm | |
| ClosedOpenInterval | Closed-open interval | |
| ConstE | The constant e (2.718...) | |
| Infinity | Positive infinity |
Source code for this entry:
Entry(ID("30bd5b"),
Formula(Equal(LambertW(Mul(x, Log(x))), Log(x))),
Variables(x),
Assumptions(Element(x, ClosedOpenInterval(Div(1, ConstE), Infinity))))