count_edges_eq_one — Mathlib

English

If an edge e belongs to the edges of the path p, then e occurs exactly once along that walk.

Русский

Если ребро e принадлежит множеству ребер пути p, то оно встречается ровно один раз на обходе.

LaTeX

$$$ [DecidableEq V] {u v : V} {p : G.Path u v} (e : Sym2 V) (hw : e \in (p : G.Walk u v).edges), (p : G.Walk u v).edges.count e = 1$$$

Lean4

theorem count_edges_eq_one [DecidableEq V] {u v : V} {p : G.Path u v} (e : Sym2 V) (hw : e ∈ (p : G.Walk u v).edges) :
    (p : G.Walk u v).edges.count e = 1 :=
  List.count_eq_one_of_mem p.property.isTrail.edges_nodup hw

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