The Tangent Function on $(-\pi/2,\pi/2)$

In the setting of The Real Line: Standing Notation and Background for Calculus on Intervals, let $\sin,\cos:\mathbb{R}\to\mathbb{R}$ be the sine and cosine functions and let $\pi$ be the number of The Number Pi (i).

(i) The tangent function. The tangent function is the function

$$\tan:(-\pi/2,\pi/2)\to\mathbb{R},\qquad \tan x=\frac{\sin x}{\cos x},$$

the quotient being defined because $\cos x>0$ for $x\in(-\pi/2,\pi/2)$, by The Cosine Is Positive on $(-\pi/2,\pi/2)$ (i) (a function by Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity (iii)).