flatten_splitWrtCompositionAux — Mathlib

English

If the sum of the indices ns equals the length of l, then flattening the split of l along ns returns the original list l.

Русский

Если сумма ns равна длине l, то развёртка разбиения l по ns даёт исходный список l.

LaTeX

$$$\text{ns}.\mathrm{sum} = |l| \Rightarrow (l.splitWrtCompositionAux ns).flatten = l$$$

Lean4

theorem flatten_splitWrtCompositionAux {ns : List ℕ} :
    ∀ {l : List α}, ns.sum = l.length → (l.splitWrtCompositionAux ns).flatten = l := by
  induction ns with
  | nil => exact fun h ↦ (length_eq_zero_iff.1 h.symm).symm
  | cons n ns IH =>
    intro l h; rw [sum_cons] at h
    simp only [splitWrtCompositionAux_cons]; dsimp
    rw [IH]
    · simp
    · rw [length_drop, ← h, add_tsub_cancel_left]

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