mem_cyclicPermutations_iff — Mathlib

English

For all lists l and l', l ∈ cyclicPermutations(l') if and only if l is a rotation of l'.

Русский

Для любых списков l и l' верно: l принадлежит cyclicPermutations(l') тогда и только тогда, когда l является поворотом l'.

LaTeX

$$$$l \in \operatorname{cyclicPermutations}(l') \iff l \sim_r l'. $$$$

Lean4

@[simp]
theorem mem_cyclicPermutations_iff : l ∈ cyclicPermutations l' ↔ l ~r l' :=
  by
  constructor
  · simp_rw [mem_iff_get, get_cyclicPermutations]
    rintro ⟨k, rfl⟩
    exact .forall _ _
  · rintro ⟨k, rfl⟩
    rw [cyclicPermutations_rotate, mem_rotate]
    apply mem_cyclicPermutations_self

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