TeX:
x \in \mathbb{R} \;\implies\; \operatorname{sinc}(x) \in \left(-0.217234, 1\right]Definitions:
| Fungrim symbol | Notation | Short description |
|---|---|---|
| RR | Real numbers | |
| Sinc | Sinc function | |
| OpenClosedInterval | Open-closed interval |
Source code for this entry:
Entry(ID("41998e"),
Formula(Implies(Element(x, RR), Element(Sinc(x), OpenClosedInterval(Decimal("-0.217234"), 1)))),
Variables(x))