nodup_tail_support_reverse — Mathlib

English

The tail of the support of the reverse walk is noduplicated if and only if the tail of the support of the original walk is noduplicated.

Русский

Хвост поддержки обратного хода равен устойчивому к повторениям тогда и только тогда, когда хвост поддержки исходного хода тоже не содержит повторов.

LaTeX

$$$ p.\mathrm{reverse}.\mathrm{support}.\text{tail} \ \mathrm{Nodup} \;\iff\; p.\mathrm{support}.\text{tail} \ \mathrm{Nodup} $$$

Lean4

theorem nodup_tail_support_reverse {u : V} {p : G.Walk u u} : p.reverse.support.tail.Nodup ↔ p.support.tail.Nodup :=
  by
  rw [Walk.support_reverse]
  refine List.nodup_tail_reverse p.support ?h
  rw [← getVert_eq_support_getElem? _ (by cutsat), List.getLast?_eq_getElem?, ←
    getVert_eq_support_getElem? _ (by rw [Walk.length_support]; cutsat)]
  aesop

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