Assumptions:
References:
- https://cs.stackexchange.com/q/93003
TeX:
B_{n} \ge {k}^{n - k}
n \in \mathbb{Z}_{\ge 0} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}Definitions:
| Fungrim symbol | Notation | Short description | 
|---|---|---|
| BellNumber | Bell number | |
| Pow | Power | |
| ZZGreaterEqual | Integers greater than or equal to n | 
Source code for this entry:
Entry(ID("a747a4"),
    Formula(GreaterEqual(BellNumber(n), Pow(k, Sub(n, k)))),
    Variables(n, k),
    Assumptions(And(Element(n, ZZGreaterEqual(0)), Element(k, ZZGreaterEqual(0)))),
    References("https://cs.stackexchange.com/q/93003"))