map_cons — Mathlib

English

Mapping respects the cons operation: map f (cons a v) = cons (f a) (map f v).

Русский

Отображение сохраняет операцию cons: map f (cons a v) = cons (f a) (map f v).

LaTeX

$$$\\forall f:\\alpha\\to\\beta,\\forall a:\\alpha,\\forall v:\\text{Vector}(\\alpha,n),\\ map\\ f\\ (\\text{cons } a\\ v)=\\text{cons } (f\\ a)\\ (map\\ f\\ v)$$$

Lean4

/-- `map` is natural with respect to `cons`. -/
@[simp]
theorem map_cons (f : α → β) (a : α) : ∀ v : Vector α n, map f (cons a v) = cons (f a) (map f v)
  | ⟨_, _⟩ => rfl

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