drop_take_append_drop — Mathlib

English

Swapping the summands of the previous identity yields the same relation with the added commutativity of addition.

Русский

Замена порядка слагаемых в предыдущем тождении даёт аналогичное соотношение с учётом коммутативности сложения.

LaTeX

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

Lean4

@[simp]
theorem drop_take_append_drop (x : List α) (m n : ℕ) : (x.drop m).take n ++ x.drop (m + n) = x.drop m := by
  rw [← drop_drop, take_append_drop]

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