card_filter_odd_degree — Mathlib

English

For an Eulerian walk p, the number of vertices of odd degree is either 0 or 2.

Русский

Для эйлерова пути p число вершин нечётной степени равно 0 или 2.

LaTeX

$$$ \text{Fintype.card} \{v : V \mid \text{Odd} (G.degree v)\} = 0 \;\vee\; \text{Fintype.card} \{v : V \mid \text{Odd} (G.degree v)\} = 2 $$$

Lean4

theorem card_filter_odd_degree [Fintype V] [DecidableRel G.Adj] {u v : V} {p : G.Walk u v} (ht : p.IsEulerian) {s}
    (h : s = (Finset.univ : Finset V).filter fun v => Odd (G.degree v)) : s.card = 0 ∨ s.card = 2 :=
  by
  subst s
  simp only [← Nat.not_even_iff_odd, Finset.card_eq_zero]
  simp only [ht.even_degree_iff, Ne, not_forall, not_and, Classical.not_not, exists_prop]
  obtain rfl | hn := eq_or_ne u v
  · simp
  · right
    convert_to _ = ({ u, v } : Finset V).card
    · simp [hn]
    · congr
      ext x
      simp [hn, imp_iff_not_or]

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