English
If G ≤ G' (G embedded in G'), then the number of odd components in G' is no larger than in G.
Русский
Если граф G входит в граф G', то число нечетных компонент в G' не превосходит числа нечетных компонент в G.
LaTeX
$$∀ {G' : SimpleGraph V}, h : G ≤ G' → G'.oddComponents.ncard ≤ G.oddComponents.ncard$$
Lean4
theorem ncard_oddComponents_mono [Finite V] {G' : SimpleGraph V} (h : G ≤ G') :
G'.oddComponents.ncard ≤ G.oddComponents.ncard :=
by
have aux (c : G'.ConnectedComponent) (hc : Odd c.supp.ncard) :
{c' : G.ConnectedComponent | Odd c'.supp.ncard ∧ c'.supp ⊆ c.supp}.Nonempty :=
by
refine Set.nonempty_of_ncard_ne_zero fun h' ↦ ?_
simpa [-Nat.card_eq_fintype_card, -Set.coe_setOf, h'] using (c.odd_oddComponents_ncard_subset_supp _ h).2 hc
let f : G'.oddComponents → G.oddComponents := fun ⟨c, hc⟩ ↦ ⟨(aux c hc).choose, (aux c hc).choose_spec.1⟩
refine Nat.card_le_card_of_injective f fun c c' fcc' ↦ ?_
simp only [Subtype.mk.injEq, f] at fcc'
exact
Subtype.val_injective
(ConnectedComponent.eq_of_common_vertex
((fcc' ▸ (aux c.1 c.2).choose_spec.2) (ConnectedComponent.nonempty_supp _).some_mem)
((aux c'.1 c'.2).choose_spec.2 (ConnectedComponent.nonempty_supp _).some_mem))
