Assumptions:
TeX:
\sin(x) \ge \frac{x \left(\pi - x\right)}{\pi} x \in \left[0, \pi\right]
Definitions:
Fungrim symbol | Notation | Short description |
---|---|---|
Sin | Sine | |
Pi | The constant pi (3.14...) | |
ClosedInterval | Closed interval |
Source code for this entry:
Entry(ID("d38739"), Formula(GreaterEqual(Sin(x), Div(Mul(x, Sub(Pi, x)), Pi))), Variables(x), Assumptions(Element(x, ClosedInterval(0, Pi))))