even_ncard_supp_sdiff_rep — Mathlib

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

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