toSubgraph_append — Mathlib

English

For walks p : G.Walk u v and q : G.Walk v w, the toSubgraph of their concatenation equals the join of their toSubgraphs.

Русский

Для ходов p: G.Walk u v и q: G.Walk v w, подграф, полученный из их конкатенации, равен объединению их подграфов.

LaTeX

$$$ (p.append q).toSubgraph = p.toSubgraph \sqcup q.toSubgraph $$$

Lean4

@[simp]
theorem toSubgraph_append (p : G.Walk u v) (q : G.Walk v w) : (p.append q).toSubgraph = p.toSubgraph ⊔ q.toSubgraph :=
  by induction p <;> simp [*, sup_assoc]

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