mem_tail_support_append_iff — Mathlib

English

For a walk p from u to v and a walk p' from v to w, the tail of the support of their concatenation is exactly the union of the tails of p and p'.

Русский

Для обхода p: u→v и обхода p': v→w сумма хвостов их поддержек равна хвостам конкатенированного обхода.

LaTeX

$$$t\in (p\append p').\mathrm{support}.\mathrm{tail} \iff t\in p.\mathrm{support}.\mathrm{tail} \lor t\in p'.\mathrm{support}.\mathrm{tail}$$$

Lean4

@[simp]
theorem mem_tail_support_append_iff {t u v w : V} (p : G.Walk u v) (p' : G.Walk v w) :
    t ∈ (p.append p').support.tail ↔ t ∈ p.support.tail ∨ t ∈ p'.support.tail := by
  rw [tail_support_append, List.mem_append]

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