Arc length / sector area formulas

Dependencies: Central ∠, arc, chord are pairwise equivalent (central angle ⇔ chord ⇔ arc) + Protractor axiom (angle additivity) + the circumference formula $C = 2\pi r$ and the area formula $S_\circ = \pi r^2$ (these two are quoted as basic formulas, not as separate theorem nodes).

Statement

Let $\odot O$ have radius $r$, and let $\alpha$ be a central angle (measured in radians, $\alpha\in[0,\,2\pi]$). Then on the corresponding sector:

Here $\ell(\alpha)$ is the arc length of that arc, and $S(\alpha)$ is the area of the corresponding sector (the region enclosed by the two radii and that arc).