English
The number of vertices of odd degree is even.
Русский
Чётность числа вершин нечетной степени: их число четно.
LaTeX
$$$\operatorname{Even}\left(\#\{v : V \mid \operatorname{Odd}(G.degree(v))\}\right)$$$
Lean4
/-- The handshaking lemma. See also `SimpleGraph.sum_degrees_eq_twice_card_edges`. -/
theorem even_card_odd_degree_vertices [Fintype V] [DecidableRel G.Adj] : Even #{v | Odd (G.degree v)} := by
classical
have h := congr_arg (fun n => ↑n : ℕ → ZMod 2) G.sum_degrees_eq_twice_card_edges
simp only [ZMod.natCast_self, zero_mul, Nat.cast_mul] at h
rw [Nat.cast_sum, ← sum_filter_ne_zero] at h
rw [sum_congr (g := fun _v ↦ (1 : ZMod 2)) rfl] at h
· simp only [mul_one, nsmul_eq_mul, sum_const, Ne] at h
rw [← ZMod.natCast_eq_zero_iff_even]
convert h
exact ZMod.natCast_ne_zero_iff_odd.symm
· intro v
rw [mem_filter_univ, Ne, ZMod.natCast_eq_zero_iff_even, ZMod.natCast_eq_one_iff_odd, ← Nat.not_even_iff_odd]
tauto
