rotate_eq_drop_append_take — Mathlib

English

If n ≤ length(l), then l.rotate n = l.drop n ++ l.take n.

Русский

Если n ≤ длина(l), тогда l.rotate n = l.drop n ++ l.take n.

LaTeX

$$$\\forall \\alpha \\in \\mathsf{Type},\\ {l : \\mathsf{List}(\\alpha)}{n : \\mathbb{N}},\\ n \\leq \\operatorname{length}(l) \\Rightarrow l.rotate n = l.drop n ++ l.take n$$$

Lean4

theorem rotate_eq_drop_append_take {l : List α} {n : ℕ} : n ≤ l.length → l.rotate n = l.drop n ++ l.take n := by
  rw [rotate_eq_rotate']; exact rotate'_eq_drop_append_take

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