mem_rotate — Mathlib

English

An element a appears in l.rotate n if and only if it appears in l.

Русский

Элемент a встречается в l.rotate n тогда и только тогда, когда он встречается в l.

LaTeX

$$$\\forall \\alpha \\in \\mathsf{Type},\\forall l \\in \\mathsf{List}(\\alpha),\\forall a \\in \\alpha,\\ (a \\in l.rotate n) \\Leftrightarrow (a \\in l)$$$

Lean4

@[simp]
theorem mem_rotate : ∀ {l : List α} {a : α} {n : ℕ}, a ∈ l.rotate n ↔ a ∈ l
  | [], _, n => by simp
  | a :: l, _, 0 => by simp
  | a :: l, _, n + 1 => by simp [rotate_cons_succ, mem_rotate, or_comm]

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