English
A component with universal vertices remains even after removing representatives of odd components and a subset of universal vertices.
Русский
Компонент графа с универсальными вершинами остается четным после удаления представителей нечетных компонент и подмножества универсальных вершин.
LaTeX
$$Even (image of K.supp \ (s ∪ t)).ncard$$
Lean4
/-- A component of the graph with universal vertices is even if we remove a set of representatives
of odd components and a subset of universal vertices.
This is because the number of vertices in the even components is not affected, and from odd
components exactly one vertex is removed. -/
theorem even_ncard_image_val_supp_sdiff_image_val_rep_union {t : Set V} {s : Set G.deleteUniversalVerts.verts}
(K : G.deleteUniversalVerts.coe.ConnectedComponent) (h : t ⊆ G.universalVerts)
(hrep : ConnectedComponent.Represents s G.deleteUniversalVerts.coe.oddComponents) :
Even (Subtype.val '' K.supp \ (Subtype.val '' s ∪ t)).ncard := by
simp [-deleteUniversalVerts_verts, ← Set.diff_inter_diff, ← Set.image_diff Subtype.val_injective,
sdiff_eq_left.mpr <| Set.disjoint_of_subset_right h (disjoint_image_val_universalVerts _),
Set.inter_diff_distrib_right, ← Set.image_inter Subtype.val_injective,
Set.ncard_image_of_injective _ Subtype.val_injective, K.even_ncard_supp_sdiff_rep hrep]
