English
Mapping a function over a list built by cons distributes as cons of mapped head and mapped tail: (l.cons a).map f = (l.map f).cons (f a).
Русский
Отображение функции над списком, построенным конструктором cons, распадается на конc головки и отображение хвоста: (l.cons a).map f = (l.map f).cons (f a).
LaTeX
$$$\forall {\Gamma \Gamma'} [Inhabited(\Gamma)] [Inhabited(\Gamma')] (f : PointedMap(\Gamma, \Gamma')) (l : ListBlank(\Gamma)) (a : \Gamma): (l.cons a).map f = (l.map f).cons (f a)$$$
Lean4
@[simp]
theorem map_cons {Γ Γ'} [Inhabited Γ] [Inhabited Γ'] (f : PointedMap Γ Γ') (l : ListBlank Γ) (a : Γ) :
(l.cons a).map f = (l.map f).cons (f a) :=
by
refine (ListBlank.cons_head_tail _).symm.trans ?_
simp only [ListBlank.head_map, ListBlank.head_cons, ListBlank.tail_map, ListBlank.tail_cons]
