I'm working on some documentation for a system that uses an arbitrary waveform generator that accepts data with a number of requirements. I would like to include some formal definitions of the requirements for academic readers, as well as an exercise for myself.
The device requires a set of between 128 and 8 million elements (inclusive), the number of elements must also be a multiple of 8. Each element in the set must be an even integer between -32768 and 32766 (inclusive).
I've put together what I think is correct(ish?), but I'm not sure if I'm mixing and matching conventions because I've looked at many different sources for reference. I was unable to find an example of a set-builder definition that both described the restrictions on the size of the set as well as the elements within the set.
This is what I have:
$$ S = \{v_{1},v_{2},v_{3},...,v_{n} : \exists a \in \mathbb{Z} s.t. n=8a\wedge128\le n \le 8000000\wedge\forall v \in S( \exists b \in \mathbb{Z} s.t. v=2b\wedge-32768\le v \le 32766)\} $$
First off, is this correct? Secondly, is this an advisable way to define this set via set-builder notation?
To be clear, the documentation will also contain a "plain english" definition of the set, similar to my second paragraph. Having a formally notated definition of this set isn't a strict requirement, but I'd like to know with certainty for my own benefit how to express this formally if it were.