edgeSet_append — Mathlib

English

If p is a walk from u to v and q is a walk from v to w, then the edge set of the concatenation p.append q equals the union of the edge sets of p and q.

Русский

Пусть p — ход из u в v, а q — ход из v в w. Тогда множество рёбер пути p.append q равно объединению множеств рёбер p и q.

LaTeX

$$$ (p \append q).edgeSet = p.edgeSet \cup q.edgeSet $$$

Lean4

theorem edgeSet_append {u v w : V} (p : G.Walk u v) (q : G.Walk v w) : (p.append q).edgeSet = p.edgeSet ∪ q.edgeSet :=
  by ext; simp

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