splitWrtComposition_flatten — Mathlib

English

If you join a list of lists and then split the flattening along the same composition, you obtain the original list of lists.

Русский

Если соединить список списков и затем разложить получившуюся плоскую последовательность по той же композиции, получится исходный список списков.

LaTeX

$$$splitWrtComposition(flatten\, L) \;=\; L$ при соответствующих c.blocks$$$

Lean4

/-- If one joins a list of lists and then splits the flattening along the right composition,
one gets back the original list of lists. -/
@[simp]
theorem splitWrtComposition_flatten (L : List (List α)) (c : Composition L.flatten.length)
    (h : map length L = c.blocks) : splitWrtComposition (flatten L) c = L := by
  simp only [and_self_iff, eq_iff_flatten_eq, flatten_splitWrtComposition, map_length_splitWrtComposition, h]

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