English
Let K be a connected component and hrep a representation of s by the odd components. Then (K.supp \\ s).ncard is even.
Русский
Пусть K — компонент связности, а hrep — представление s через нечетные компоненты. Тогда (K.supp \\ s).ncard четно.
LaTeX
$$$ \\operatorname{Even} (K.supp \\ s).ncard $$$
Lean4
theorem even_ncard_supp_sdiff_rep {s : Set V} (K : G.ConnectedComponent)
(hrep : ConnectedComponent.Represents s G.oddComponents) : Even (K.supp \ s).ncard :=
by
by_cases h : Even K.supp.ncard
· simpa [hrep.ncard_sdiff_of_notMem (by simpa [Set.ncard_image_of_injective, ← Nat.not_odd_iff_even] using h)] using h
· have : K.supp.ncard ≠ 0 := Nat.ne_of_odd_add (Nat.not_even_iff_odd.mp h)
rw [hrep.ncard_sdiff_of_mem (Nat.not_even_iff_odd.mp h), Nat.even_sub (by cutsat)]
simpa [Nat.even_sub] using Nat.not_even_iff_odd.mp h