map_tail — Mathlib

English

Mapping a function after taking the tail equals taking the tail after mapping: map f (tail s) = tail (map f s).

Русский

Преобразование после взятия хвоста равносильно взятию хвоста после отображения: map f (tail s) = tail (map f s).

LaTeX

$$$\forall {f : \alpha \to \beta},\; \forall s,\; map f (tail s) = tail (map f s)$$$

Lean4

@[simp]
theorem map_tail (f : α → β) : ∀ s, map f (tail s) = tail (map f s)
  | ⟨s, al⟩ => by apply Subtype.eq; dsimp [tail, map]

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