prev_next — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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