Assumptions:
TeX:
B_{n} \ge {\left(\frac{n}{e \log(n)}\right)}^{n}
n \in \mathbb{Z}_{\ge 2}Definitions:
| Fungrim symbol | Notation | Short description |
|---|---|---|
| BellNumber | Bell number | |
| Pow | Power | |
| ConstE | The constant e (2.718...) | |
| Log | Natural logarithm | |
| ZZGreaterEqual | Integers greater than or equal to n |
Source code for this entry:
Entry(ID("468def"),
Formula(GreaterEqual(BellNumber(n), Pow(Div(n, Mul(ConstE, Log(n))), n))),
Variables(n),
Assumptions(Element(n, ZZGreaterEqual(2))))