Kit for def:tangent

In the setting of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity, let $n\ge1$ be a metatheoretic number, let $x_{0},\dots,x_{n-1}$ be distinct set variables, and let $i<n$. The first clause states that a condition on $x_{0},\dots,x_{n-1}$ is predicative: expressed by a predicative formula, with $x_{0},\dots,x_{n-1}$ in place of the variables $x_{1},\dots,x_{k}$ of Conditions Expressed by a Predicative Formula, and Guards (i) and no displayed variables; $\mathbb{N}$ and its element $1$, the addition of $\mathbb{N}_{0}$, the set $\mathbb{C}$ of complex numbers with its sum and product operations of The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (iii), its unit $1$ (The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers (ii)) and its imaginary unit, the map $\mathbb{R}\to\mathbb{C}$ of The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (vi), the distance $d_{\mathbb{C}}$ on $\mathbb{C}$, and $\mathbb{R}$ with its order $\le$, its strict order $<$, its addition $+$ and multiplication $\cdot$ of The Real Numbers (iii), its element $0$ and its element $\pi$ of The Number Pi (i) are parameters. In both clauses, "the tangent function" means the function $\tan$ of The Tangent Function on $(-\pi/2,\pi/2)$ (i).

(i) The tangent. The condition "$x_{i}$ is the tangent function" on $x_{0},\dots,x_{n-1}$ is predicative.

(ii) A class for the tangent. There is a class $T$ such that, for every class $a$, $a\in T$ if and only if $a$ is the tangent function.