coe_support_append' — Mathlib

English

If a graph walk contains an edge s(x,y), then x is adjacent to y in the graph.

Русский

Если обход содержит ребро s(x,y), то x смежен с y в графе.

LaTeX

$$$\text{if } s(x,y) \in p.\mathrm{edges} \text{ then } G.\mathrm{Adj}\\ x\\ y$$$

Lean4

theorem coe_support_append' [DecidableEq V] {u v w : V} (p : G.Walk u v) (p' : G.Walk v w) :
    ((p.append p').support : Multiset V) = p.support + p'.support - { v } :=
  by
  rw [support_append, ← Multiset.coe_add]
  simp only [coe_support]
  rw [add_comm ({ v } : Multiset V)]
  simp only [← add_assoc, add_tsub_cancel_right]

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