English
For a finite graph, the parity of the number of odd components equals the parity of the cardinality of the vertex set V.
Русский
Для конечного графа нечетность числа нечетных компонент равна нечетности мощности множества вершин графа.
LaTeX
$$∀ {G} [Finite V], Odd G.oddComponents.ncard ↔ Odd (Nat.card V)$$
Lean4
theorem odd_ncard_oddComponents [Finite V] : Odd G.oddComponents.ncard ↔ Odd (Nat.card V) := by
classical
cases nonempty_fintype V
rw [Nat.card_eq_fintype_card]
simp only [← (set_fintype_card_eq_univ_iff _).mpr G.iUnion_connectedComponentSupp, ← Set.toFinset_card,
Set.toFinset_iUnion ConnectedComponent.supp]
rw [Finset.card_biUnion
(fun x _ y _ hxy ↦ Set.disjoint_toFinset.mpr (pairwise_disjoint_supp_connectedComponent _ hxy))]
simp_rw [← Set.ncard_eq_toFinset_card', ← Finset.coe_filter_univ, Set.ncard_coe_finset]
exact (Finset.odd_sum_iff_odd_card_odd (fun x : G.ConnectedComponent ↦ x.supp.ncard)).symm
