tprod — Mathlib

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

Похожие утверждения