isEulerian_iff — Mathlib

English

If p is a trail, then p is Eulerian if and only if p.edgeSet equals G.edgeSet.

Русский

Если p является трелью, то p эйлеров тогда и только тогда, когда множество рёбер p.edgeSet равно множеству рёбер G.

LaTeX

$$hp : p.IsTrail ⟹ (p.IsEulerian \iff p.edgeSet = G.edgeSet)$$

Lean4

theorem isEulerian_iff {u v : V} {p : G.Walk u v} (hp : p.IsTrail) : p.IsEulerian ↔ p.edgeSet = G.edgeSet :=
  ⟨fun h ↦ Set.Subset.antisymm p.edges_subset_edgeSet (p.isEulerian_iff.mp h).2, fun h ↦
    p.isEulerian_iff.mpr ⟨hp, by simp [← h]⟩⟩

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