length_revzip

Mathlib.Data.List.Zip

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

English

The length of revzip l equals the length of l.

Русский

Длина revzip l равна длине l.

LaTeX

$$$\operatorname{length}(\operatorname{revzip}\ l) = \operatorname{length}(l)$$$

Lean4

@[simp]
theorem length_revzip (l : List α) : length (revzip l) = length l := by
  simp only [revzip, length_zip, length_reverse, min_self]

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

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

Разделы

Аффилиация

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