Theorems · Theorem · combinatorics

SimpleGraph.even_ncard_image_val_supp_sdiff_image_val_rep_union

∀ {V : Type u_1} {G : SimpleGraph V} {t : Set V} {s : Set ↑G.deleteUniversalVerts.verts}
  (K : G.deleteUniversalVerts.coe.ConnectedComponent),
  t ⊆ G.universalVerts →
    SimpleGraph.ConnectedComponent.Represents s G.deleteUniversalVerts.coe.oddComponents →
      Even (Subtype.val '' K.supp \ (Subtype.val '' s ∪ t)).ncard

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.

Defined in

Mathlib.Combinatorics.SimpleGraph.UniversalVerts

Cited by

0 results in Mathlib

Foundations

Depth 104 from the axioms · uses propext, Classical.choice, Quot.sound