map_cons — Mathlib

English

The map distributes over the cons constructor: map f (cons a s) = cons (f a) (map f s).

Русский

Отображение распределяется по конструктору cons: map f (cons a s) = cons (f a) (map f s).

LaTeX

$$$$ \\operatorname{map} f (\\operatorname{cons}} a s) = \\operatorname{cons} (f a) (\\operatorname{map} f s) $$$$

Lean4

@[simp]
theorem map_cons (f : α → β) (a s) : map f (cons a s) = cons (f a) (map f s) :=
  Seq.map_cons _ _ _

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