toList_formPerm_isRotated_self — Mathlib

English

If l has length at least 2 and is nodup, then for any x in l, toList (formPerm l) x is a rotation of l.

Русский

Если список l имеет длину ≥ 2 и не содержит повторов, то для любого x ∈ l toList (formPerm l) x является поворотом списка l.

LaTeX

$$$$hl:\ge 2 \land hn:\mathrm{Nodup}(l) \Rightarrow \forall x\in l,\ (l.formPerm\ toList\ x)\, IsRotated\ l.$$$$

Lean4

theorem toList_formPerm_isRotated_self (l : List α) (hl : 2 ≤ l.length) (hn : Nodup l) (x : α) (hx : x ∈ l) :
    toList (formPerm l) x ~r l := by
  obtain ⟨k, hk, rfl⟩ := get_of_mem hx
  have hr : l ~r l.rotate k := ⟨k, rfl⟩
  rw [formPerm_eq_of_isRotated hn hr]
  rw [get_eq_get_rotate l k k]
  simp only [Nat.mod_eq_of_lt k.2, tsub_add_cancel_of_le (le_of_lt k.2), Nat.mod_self]
  rw [toList_formPerm_nontrivial]
  · simp
  · simpa using hl
  · simpa using hn

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