edgeSet_cons — Mathlib

English

If p is a walk from v to w and h is an adjacency between u and v, then the edgeSet of cons(h,p) is the insert of s(u,v) into p.edgeSet.

Русский

Если p — ход от v к w, а h — переход между u и v, то edgeSet(cons(h,p)) равен вставке s(u,v) в edgeSet(p).

LaTeX

$$$ (\text{cons} \; h\, p).edgeSet = \text{insert} \, s(u,v) \, p.edgeSet $$$

Lean4

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

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