next_reverse_eq_prev — Mathlib

English

In a cyclic order with no repetitions, the successor of x in the reversed cycle equals the predecessor of x in the original cycle.

Русский

Во циклическом порядке без повторов преемник элемента x в обращённом цикле равен его предшественнику в исходном цикле.

LaTeX

$$$$ s^{-1}.next\\bigl(\\operatorname{nodup\\_reverse\\_iff}(hs)\\bigr)\\ x\\ (\\operatorname{mem\\_reverse\\_iff}(hx)) = s.prev(hs)\\ x\\ hx. $$$$

Lean4

theorem next_reverse_eq_prev (s : Cycle α) (hs : Nodup s) (x : α) (hx : x ∈ s) :
    s.reverse.next (nodup_reverse_iff.mpr hs) x (mem_reverse_iff.mpr hx) = s.prev hs x hx := by
  simp [← prev_reverse_eq_next]

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