map_reverseAux — Mathlib

English

For any f and lists l1, l2, map f distributes over reverseAux.

Русский

Для любой функции f и списков l1, l2 отображение f распределяется над reverseAux.

LaTeX

$$$\\\\mathrm{map}\\\\ f \\\\ (\\\\mathrm{reverseAux}\\\\ l_1\\\\ l_2) = \\\\mathrm{reverseAux}(\\\\mathrm{map}\\\\ f\\\\ l_1)\\\\ (\\\\mathrm{map}\\\\ f\\\\ l_2)$$$

Lean4

theorem map_reverseAux (f : α → β) (l₁ l₂ : List α) : map f (reverseAux l₁ l₂) = reverseAux (map f l₁) (map f l₂) := by
  simp only [reverseAux_eq, map_append, map_reverse]
    -- TODO: Rename `List.reverse_perm` to `List.reverse_perm_self`

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