Theorems · Theorem · combinatorics

List.Vector.map_cons

∀ {α : Type u_1} {β : Type u_2} {n : ℕ} (f : α → β) (a : α) (v : List.Vector α n),
  List.Vector.map f (a ::ᵥ v) = f a ::ᵥ List.Vector.map f v

map is natural with respect to cons.

Defined in

Mathlib.Data.Vector.Defs

Cited by

6 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext