isRotated_prev_eq — Mathlib

English

If l ~r l' and x ∈ l, then the predecessor of x in l equals the predecessor of x in l' (under the corresponding membership).

Русский

Если l ~r l' и x ∈ l, то предшественник x в l равен предшественнику x в l' (при соответствующем переносе принадлежности).

LaTeX

$$$l.prev\ x\ hx = l'.prev\ x (h.mem\_iff.mp hx)$$$

Lean4

theorem isRotated_prev_eq {l l' : List α} (h : l ~r l') (hn : Nodup l) {x : α} (hx : x ∈ l) :
    l.prev x hx = l'.prev x (h.mem_iff.mp hx) :=
  by
  rw [← next_reverse_eq_prev _ hn, ← next_reverse_eq_prev _ (h.nodup_iff.mp hn)]
  exact isRotated_next_eq h.reverse (nodup_reverse.mpr hn) _

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