smallVector — Mathlib

English

For any α and n, if α is Small then List.Vector α n is Small.

Русский

Для любого α и натурального числа n, если α мала, то List.Vector α n мала.

LaTeX

$$$\forall \alpha, \forall n:\\mathbb{N}, Small(\alpha) \Rightarrow Small(\mathrm{List.Vector}(\alpha,n)).$$$

Lean4

instance smallVector {α : Type v} {n : ℕ} [Small.{u} α] : Small.{u} (List.Vector α n) :=
  small_of_injective (Equiv.vectorEquivFin α n).injective

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