Arrow — Mathlib

English

An arrow from α to β in TypeVec n is a family of maps f_i: α(i) → β(i) indexed by i ∈ Fin2 n.

Русский

Стрелка от α к β в TypeVec n — это семейство отображений f_i: α(i) → β(i), индексируемое i ∈ Fin2 n.

LaTeX

$$$\\text{Arrow}(\\alpha,\\beta) = \\forall i : \\mathrm{Fin}_2(n), \\alpha(i) \\to \\beta(i)$$$

Lean4

/-- arrow in the category of `TypeVec` -/
def Arrow (α β : TypeVec n) :=
  ∀ i : Fin2 n, α i → β i

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