Given this definition:
Definition 2.1. An alphabet $\Sigma$ is said to be ranked if for each nonnegative integer $k$ a subset $\Sigma_k$ of $\Sigma$ is specified, such that $\Sigma_k$ is nonempty for a finite number of $k$'s only, and such that $\Sigma= \bigcup_{k \ge 0} \Sigma_k$. $^\dagger$
How would you write that more formally using things like $\forall k \in \mathbb{N},\dots$? I am having a hard time seeing how to turn this into a more formalized version which I could then figure out how to translate into something like Coq.