length_splitLengths

Mathlib.Data.List.SplitLengths

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

English

The length of the splitLengths partition equals the number of chunks sz.

Русский

Длина разбиения splitLengths равна количеству фрагментов sz.

LaTeX

$$$(sz.splitLengths l).length = sz.length$$$

Lean4

@[simp]
theorem length_splitLengths : (sz.splitLengths l).length = sz.length := by
  induction sz generalizing l <;> simp [splitLengths, *]

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

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

Разделы

Аффилиация

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