Theorems · Theorem · combinatorics

SimpleGraph.Walk.IsEulerian.card_filter_odd_degree

∀ {V : Type u_1} {G : SimpleGraph V} [inst : DecidableEq V] [inst_1 : Fintype V] [inst_2 : DecidableRel G.Adj] {u v : V}
  {p : G.Walk u v}, p.IsEulerian → ∀ {s : Finset V}, s = {v | Odd (G.degree v)} → s.card = 0 ∨ s.card = 2

Defined in

Mathlib.Combinatorics.SimpleGraph.Trails

Cited by

1 results in Mathlib

Foundations

Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqFintypeDecidableRel