English
If a vertex v has odd degree, there exists another vertex w ≠ v with odd degree.
Русский
Если вершина v имеет нечетную степень, существует другая вершина w ≠ v с нечетной степенью.
LaTeX
$$$\operatorname{Odd}(G.degree(v)) \rightarrow \exists w \neq v \; \operatorname{Odd}(G.degree(w))$$$
Lean4
theorem odd_card_odd_degree_vertices_ne [Fintype V] [DecidableEq V] [DecidableRel G.Adj] (v : V)
(h : Odd (G.degree v)) : Odd #{w | w ≠ v ∧ Odd (G.degree w)} :=
by
rcases G.even_card_odd_degree_vertices with ⟨k, hg⟩
have hk : 0 < k :=
by
have hh : Finset.Nonempty {v : V | Odd (G.degree v)} :=
by
use v
rw [mem_filter_univ]
exact h
rwa [← card_pos, hg, ← two_mul, mul_pos_iff_of_pos_left] at hh
exact zero_lt_two
have hc : (fun w : V => w ≠ v ∧ Odd (G.degree w)) = fun w : V => Odd (G.degree w) ∧ w ≠ v :=
by
ext w
rw [and_comm]
simp only [hc]
rw [← filter_filter, filter_ne', card_erase_of_mem]
· refine ⟨k - 1, tsub_eq_of_eq_add <| hg.trans ?_⟩
cutsat
· rwa [mem_filter_univ]
