English
There is a left projection fst from a product vector α ⊗ β to α, defined recursively along the vector structure, yielding the first component as you descend the vector.
Русский
Существует левый проекционный отображение fst от вектора-произведения α ⊗ β к α, определяющее первую компоненту по структуре вектора.
LaTeX
$$$\\mathrm{fst} : \\forall {n} \\{\\alpha,\\beta : TypeVec\, n\\}, \\alpha \\otimes \\beta \\Rightarrow \\alpha.$$$
Lean4
/-- left projection of a `prod` vector -/
def fst : ∀ {n} {α β : TypeVec.{u} n}, α ⊗ β ⟹ α
| succ _, α, β, Fin2.fs i => @prod.fst _ (drop α) (drop β) i
| succ _, _, _, Fin2.fz => Prod.fst
