isEulerian_of_forall_mem — Mathlib

English

If p is a trail and every edge of G lies in p.edges, then p is Eulerian.

Русский

Если p — трель и каждое ребро графа G принадлежит p.edges, то p эйлеров.

LaTeX

$$$ p.IsTrail \land (\forall e, e \in G.edgeSet \rightarrow e \in p.edges) \Rightarrow p.IsEulerian $$$

Lean4

theorem isEulerian_of_forall_mem {u v : V} {p : G.Walk u v} (h : p.IsTrail) (hc : ∀ e, e ∈ G.edgeSet → e ∈ p.edges) :
    p.IsEulerian := fun e he => List.count_eq_one_of_mem h.edges_nodup (hc e he)

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