formPerm_apply_mem_eq_next — Mathlib

English

For a nodup l and element x in l, formPerm l x equals the next element in the cycle.

Русский

Для безповторного списка l и элемента x из l, formPerm l x равен следующему элементу цикла.

LaTeX

$$$\\text{formPerm\_apply\_mem\_eq\_next}(l,hx):\\quad \\text{formPerm } l \\ x = \\text{next } l \\ x\\ (hx)$$$

Lean4

theorem formPerm_apply_mem_eq_next (hl : Nodup l) (x : α) (hx : x ∈ l) : formPerm l x = next l x hx :=
  by
  obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx
  rw [next_getElem _ hl, formPerm_apply_getElem _ hl]

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