count_edges_le_one — Mathlib

English

In a trail p, every edge e appears at most once: p.edges.count e ≤ 1 for all e.

Русский

В траиле p каждое ребро e встречается не более одного раза: p.edges.count e ≤ 1 для любого e.

LaTeX

$$$ \forall e,\ p.IsTrail \Rightarrow p.edges.count(e) \le 1 $$$

Lean4

theorem count_edges_le_one [DecidableEq V] {u v : V} {p : G.Walk u v} (h : p.IsTrail) (e : Sym2 V) :
    p.edges.count e ≤ 1 :=
  List.nodup_iff_count_le_one.mp h.edges_nodup e

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