reverse_revzip

Mathlib.Data.List.Zip

URI: https://scilib.ai/kg/mathlib#List.reverse_revzip

← MathLib Explorer

English

Reverse of revzip l equals revzip of reverse l.

Русский

Обращение revzip l равно revzip от обратного l.

LaTeX

$$$\operatorname{reverse}\ l.\revzip = \operatorname{revzip}(l.\text{reverse})$$$

Lean4

theorem reverse_revzip (l : List α) : reverse l.revzip = revzip l.reverse :=
  by
  rw [← zip_unzip (revzip l).reverse]
  simp [unzip_eq_map, revzip, map_reverse, map_fst_zip, map_snd_zip]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru