unzip_revzip

Mathlib.Data.List.Zip

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

English

Applying unzip to revzip of l gives (l, reverse l).

Русский

Применение unzip к revzip l дает (l, reverse l).

LaTeX

$$$(revzip\ l).unzip = (l, l.reverse)$$$

Lean4

@[simp]
theorem unzip_revzip (l : List α) : (revzip l).unzip = (l, l.reverse) :=
  unzip_zip length_reverse.symm

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

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

Разделы

Аффилиация

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