sublists'_eq_sublists

Mathlib.Data.List.Sublists

URI: https://scilib.ai/kg/mathlib#List.sublists'_eq_sublists

English

sublists' l equals map reverse (sublists (reverse l)).

Русский

sublists' l = map reverse (sublists (reverse l)).

LaTeX

$$$\\text{sublists}'(l) = \\text{map}(\\text{reverse})(\\text{sublists}(\\text{reverse}(l)))$$$

Lean4

theorem sublists'_eq_sublists (l : List α) : sublists' l = map reverse (sublists (reverse l)) := by
  rw [← sublists'_reverse, reverse_reverse]

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

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

Разделы

Аффилиация

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