TeX:
z \in \mathbb{R} \;\implies\; {e}^{z} \in \left(0, \infty\right)Definitions:
| Fungrim symbol | Notation | Short description | 
|---|---|---|
| RR | Real numbers | |
| Exp | Exponential function | |
| OpenInterval | Open interval | |
| Infinity | Positive infinity | 
Source code for this entry:
Entry(ID("819b5f"),
    Formula(Implies(Element(z, RR), Element(Exp(z), OpenInterval(0, Infinity)))),
    Variables(z))