Separating transcendence basis and separably generated extensions

Let $k\subseteq K$ be a field extension and let $S\subseteq K$ be algebraically independent over $k$ (Algebraic and transcendental elements and algebraic extensions). If $K$ is algebraic over the subfield $k(S)$ generated by $S$, then $S$ is a transcendence basis of $K$ over $k$; by A maximal algebraically independent set is a transcendence basis an algebraically independent subset that is maximal for inclusion among algebraically independent subsets automatically has this property, so that lemma and this definition describe the same notion.

Now assume that $K\mathrm{/}k$ is finitely generated (Finitely generated field extensions $F(a_1,\dots ,a_r)$), say $K=k({\alpha }_1,\dots ,{\alpha }_n)$. A finite tuple of pairwise distinct elements $t_1,\dots ,t_r\in K$ is a separating transcendence basis of $K\mathrm{/}k$ when $\{t_1,\dots ,t_r\}$ is a transcendence basis of $K$ over $k$ and the extension $K\mathrm{/}k(t_1,\dots ,t_r)$ is finite separable (Separable algebraic elements and separable extensions). The extension $K\mathrm{/}k$ is separably generated over $k$, or simply separably generated, when it admits a separating transcendence basis; in this terminology a finitely generated extension is separably generated precisely when it has a transcendence basis over which its residual extension is separable.

Finiteness of the residual extension is automatic: $K$ is finitely generated over $k$, hence over $k(t_1,\dots ,t_r)$, and algebraic there by the definition of a transcendence basis, so $K\mathrm{/}k(t_1,\dots ,t_r)$ is finite by An extension generated by finitely many algebraic elements is finite. Three conventions are part of the definition.

1. The empty tuple is allowed: $r=0$ is a separating transcendence basis exactly when $K\mathrm{/}k$ is algebraic and separable, equivalently (under the finite-generation hypothesis) when $K\mathrm{/}k$ is finite separable.
2. The notion concerns $K\mathrm{/}k(t_1,\dots ,t_r)$ and says nothing about the intermediate field $k(t_1,\dots ,t_r)$ being perfect. If $k$ is perfect, the rational function field $k(t_1,\dots ,t_r)$ is nevertheless imperfect in characteristic $p$ as soon as $r\ge 1$, so separability over it is a genuine restriction and cannot be replaced by separability of algebraic extensions of $k$.
3. All transcendence bases of a finitely generated extension have the same finite cardinality $r$, namely the transcendence degree, so the number of elements in a separating transcendence basis is determined by the extension.