edgeSet_concat — Mathlib

English

Let G be a simple graph. If p is a walk from u to v and h is an adjacent edge from v to w, then the edge set of the concatenated walk p.concat h is obtained from the edge set of p by inserting the edge {v,w}.

Русский

Пусть G — простой граф. Пусть p — ход из u в v, а h — смежное ребро из v в w. Тогда множество рёбер пути p.concat h получается из множества рёбер p добавлением ребра {v,w}.

LaTeX

$$$ (p \concat h).edgeSet = p.edgeSet \cup \{ \{v,w\} \} $$$

Lean4

@[simp]
theorem edgeSet_concat {u v w : V} (p : G.Walk u v) (h : G.Adj v w) : (p.concat h).edgeSet = insert s(v, w) p.edgeSet :=
  by ext; simp [or_comm]

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