English
For finite graphs, the parity of the number of odd components inside a fixed component c' matches the parity of the cardinality of c'.supp.
Русский
Для конечного графа четность числа нечетных компонент внутри фиксированной компоненты c' совпадает с четностью мощности множества вершин c'.supp.
LaTeX
$$∀ {G'} (h : G ≤ G') (c' : G'.ConnectedComponent), Odd {c ∈ G.oddComponents | c.supp ⊆ c'.supp}.ncard ↔ Odd c'.supp.ncard$$
Lean4
theorem odd_oddComponents_ncard_subset_supp [Finite V] {G'} (h : G ≤ G') (c' : ConnectedComponent G') :
Odd {c ∈ G.oddComponents | c.supp ⊆ c'.supp}.ncard ↔ Odd c'.supp.ncard :=
by
simp_rw [← Nat.card_coe_set_eq]
classical
cases nonempty_fintype V
rw [Nat.card_eq_card_toFinset c'.supp, ← disjiUnion_supp_toFinset_eq_supp_toFinset h]
simp only [Finset.card_disjiUnion, Set.toFinset_card, Fintype.card_ofFinset]
rw [Finset.odd_sum_iff_odd_card_odd, Nat.card_eq_fintype_card, Fintype.card_ofFinset]
congr! 2
ext c
simp_rw [Set.toFinset_setOf, mem_filter, ← Set.ncard_coe_finset, coe_filter, mem_supp_iff, mem_univ, true_and, supp,
and_comm]
