snd — Mathlib

English

There is a right projection snd from α ⊗ β to β, defined recursively along the vector, yielding the second component.

Русский

Существует правое проецирование snd от α ⊗ β к β, определяемое рекурсивно вдоль вектора и возвращающее вторую компоненту.

LaTeX

$$$\\mathrm{snd} : \\forall {n} \\{\\alpha,\\beta : TypeVec\, n\\}, \\alpha \\otimes \\beta \\Rightarrow \\beta.$$$

Lean4

/-- right projection of a `prod` vector -/
def snd : ∀ {n} {α β : TypeVec.{u} n}, α ⊗ β ⟹ β
  | succ _, α, β, Fin2.fs i => @prod.snd _ (drop α) (drop β) i
  | succ _, _, _, Fin2.fz => Prod.snd

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