drop_take_append_drop' — Mathlib

English

As above, but with commutativity between m and n swapped: (x.drop m).take n ++ x.drop (n + m) = x.drop m.

Русский

Альтернативная версия: перестановка м и n даёт то же тождество: (x.drop m).take n ++ x.drop (n + m) = x.drop m.

LaTeX

$$$ (x.drop m).take n ++ x.drop (n + m) = x.drop m $$$

Lean4

/-- Compared to `drop_take_append_drop`, the order of summands is swapped. -/
@[simp]
theorem drop_take_append_drop' (x : List α) (m n : ℕ) : (x.drop m).take n ++ x.drop (n + m) = x.drop m := by
  rw [Nat.add_comm, drop_take_append_drop]

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