next_reverse_eq_prev' — Mathlib

English

For a cycle s with no duplicates on its reverse, the next element of x in s.reverse equals the previous element of x in s.reverse.

Русский

Для цикла s с безповторным перечнем на обратном цикле следующая за x величина равна предыдущей за x на обратном цикле.

LaTeX

$$$$ s.reverse.next(\\mathrm{nodup\\_reverse\\_iff.mp}(hs))\\; x\\; (\\mathrm{mem\\_reverse\\_iff.mp}(hx)) = s.reverse.prev\\; x\\; (\\mathrm{mem\\_reverse\\_iff.mp}(hx)). $$$$

Lean4

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

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