Unisolvent points exist for a linearly independent family

Let $\Bbbk$ be a field, $X$ an arbitrary type, and $\iota$ a finite type with decidable equality. Let $f : \iota \to X \to \Bbbk$ be a family of $\Bbbk$-valued functions on $X$, indexed by $\iota$, and assume that $f$ is linearly independent over $\Bbbk$ in the $\Bbbk$-vector space $X \to \Bbbk$ of all functions (with pointwise operations). The conclusion is that there exists a family of points $x : \iota \to X$, indexed by the same type $\iota$, such that the square $\iota \times \iota$ evaluation matrix whose $(i,j)$ entry is $f_j(x_i)$ has non-zero determinant, i.e. $\det\bigl(f_j(x_i)\bigr)_{i,j \in \iota} \neq 0$. No hypothesis is placed on $X$ beyond its being a type; in particular $X$ may be infinite, and no regularity or topology is involved.

This is the standard unisolvence statement: a finite linearly independent family of $\Bbbk$-valued functions admits interpolation points at which the evaluation matrix is invertible, equivalently the evaluation functionals at those points form a basis of the dual of the span. It is used in the Rankin–Selberg part of the Langlands–Tunnell input, via LanglandsTunnell.RankinSelberg.exists_unisolvence_refPoint_cutoff_of_linearIndependent_slots, to select finitely many test points at which a family of independent test data can be separated.