next_prev — Mathlib

English

Applying prev after next in a cycle returns the original element.

Русский

Применение предыдущего после следующего в цикле возвращает исходный элемент.

LaTeX

$$$$ s.next\\; hs\\; (s.prev\\; hs\\; x\\; hx)\\; (prev\\_mem\\; s\\; hs\\; x\\; hx) = x. $$$$

Lean4

@[simp]
nonrec theorem next_prev (s : Cycle α) :
    ∀ (hs : Nodup s) (x : α) (hx : x ∈ s), s.next hs (s.prev hs x hx) (prev_mem s hs x hx) = x :=
  Quotient.inductionOn' s next_prev

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