flatten_splitWrtComposition — Mathlib

English

After splitting a list along a composition and then flattening the resulting sublists, one recovers the original list.

Русский

Разделив список по композиции и затем соединив подсписки обратно, получаем исходный список.

LaTeX

$$$(l.splitWrtComposition c).flatten = l$$$

Lean4

/-- If one splits a list along a composition, and then flattens the sublists, one gets back the
original list. -/
@[simp]
theorem flatten_splitWrtComposition (l : List α) (c : Composition l.length) : (l.splitWrtComposition c).flatten = l :=
  flatten_splitWrtCompositionAux c.blocks_sum

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