English
The Set.tprod construction gives the Cartesian product of the sets along a finite index list: it is the product over i ∈ l of the sets α(i).
Русский
Конструкция Set.tprod задаёт декартово произведение множеств по конечному индексу l: это произведение множеств t(i) по i ∈ l.
LaTeX
$$$\\mathrm{Set.tprod}\\ l\\ t = \\prod_{i \\in l} t(i).$$$
Lean4
/-- A product of sets in `TProd α l`. -/
@[simp]
protected def tprod : ∀ (l : List ι) (_t : ∀ i, Set (α i)), Set (TProd α l)
| [], _ => univ
| i :: is, t => t i ×ˢ Set.tprod is t