English
There is a constructor mk for the product TypeVec α ⊗ β, which, given i ∈ Fin2 n, an element a ∈ α i and b ∈ β i, produces the product element at i, recursively defined along the vector.
Русский
Существуют конструктор mk для произведения TypeVec α ⊗ β, который, заданные i, a ∈ α i и b ∈ β i, порождает элемент произведения в позиции i, определённый рекурсивно.
LaTeX
$$$\\mathrm{mk} : \\forall {n}\\{\\alpha\\beta : TypeVec\, n\\} (i : Fin2 n), \\alpha i → \\beta i → (\\alpha \\otimes \\beta) i.$$$
Lean4
/-- constructor for `prod` -/
def mk : ∀ {n} {α β : TypeVec.{u} n} (i : Fin2 n), α i → β i → (α ⊗ β) i
| succ _, α, β, Fin2.fs i => mk (α := fun i => α i.fs) (β := fun i => β i.fs) i
| succ _, _, _, Fin2.fz => Prod.mk
