map_snoc — Mathlib

English

Applying a function to each element commutes with snoc: map f (xs.snoc x) = (map f xs).snoc (f x).

Русский

Применение функции ко всем элементам commuting с добавлением элемента в конец: map f (xs.snoc x) = (map f xs).snoc (f x).

LaTeX

$$$\text{map } f (xs.snoc x) = (\text{map } f xs).snoc (f x)$$$

Lean4

@[simp]
theorem map_snoc {f : α → β} : map f (xs.snoc x) = (map f xs).snoc (f x) := by induction xs <;> simp_all

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