map_append — Mathlib

English

Mapping distributes over concatenation: map f (append s t) = append (map f s) (map f t).

Русский

Отображение распределяется над конкатенацией: map f (append s t) = append (map f s) (map f t).

LaTeX

$$$$ \\operatorname{map} f (\\mathrm{append}} s t) = \\mathrm{append}(\\operatorname{map} f s)(\\operatorname{map} f t) $$$$

Lean4

@[simp]
theorem map_append (f : α → β) (s t) : map f (append s t) = append (map f s) (map f t) :=
  Seq.map_append _ _ _

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