count_support_eq_one — Mathlib

English

If w is in the support of the walk representing a path p from u to v, then w appears exactly once in that support.

Русский

Если вершина w принадлежит поддержке обхода, соответствующего пути p от u к v, то она встречается ровно один раз в этой поддержке.

LaTeX

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

Lean4

theorem count_support_eq_one [DecidableEq V] {u v w : V} {p : G.Path u v} (hw : w ∈ (p : G.Walk u v).support) :
    (p : G.Walk u v).support.count w = 1 :=
  List.count_eq_one_of_mem p.property.support_nodup hw

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