isEulerian_iff — Mathlib

English

For any walk p, p.IsEulerian is equivalent to p.IsTrail together with every edge of G appearing in p.edges.

Русский

Для любого пути p: эйлеровость эквивалентна тому, что pIsTrail и каждый ребро графа G встречается в p.edges.

LaTeX

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

Lean4

theorem isEulerian_iff {u v : V} (p : G.Walk u v) : p.IsEulerian ↔ p.IsTrail ∧ ∀ e, e ∈ G.edgeSet → e ∈ p.edges :=
  by
  constructor
  · intro h
    exact ⟨h.isTrail, fun _ => h.mem_edges_iff.mpr⟩
  · rintro ⟨h, hl⟩
    exact h.isEulerian_of_forall_mem hl

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