Vertex covers of multigraphs

A vertex cover of a multigraph G : Graph α β is a set of actual vertices meeting every edge: every edge has an end in the set. Parallel edges are allowed, and a loop at v is met only by sets containing v.

Main definitions

• Graph.IsVertexCover G C: the set C of actual vertices meets every edge of G.

Main results

• Graph.isVertexCover_iff_forall_exists_inc: a set of actual vertices is a vertex cover exactly when every actual edge is incident with one of its vertices.
• Graph.isVertexCover_empty_iff: the empty set is a vertex cover exactly when there are no actual edges.

def Graph.IsVertexCover {α : Type u} {β : Type v} (G : Graph α β) (C : Set ↑G.vertexSet) : Prop

The set C of actual vertices is a vertex cover of G: every edge has an end in C. A loop at v is met only by sets containing v.

theorem Graph.isVertexCover_def {α : Type u} {β : Type v} {G : Graph α β} {C : Set ↑G.vertexSet} : G.IsVertexCover C ↔ ∀ ⦃e : β⦄ ⦃x y : ↑G.vertexSet⦄, G.IsLink e ↑x ↑y → x ∈ C ∨ y ∈ C

theorem Graph.isVertexCover_iff_forall_exists_inc {α : Type u} {β : Type v} {G : Graph α β} {C : Set ↑G.vertexSet} : G.IsVertexCover C ↔ ∀ (e : ↑G.edgeSet), ∃ x ∈ C, G.Inc ↑e ↑x

A set of actual vertices is a vertex cover exactly when every actual edge is incident with one of its vertices.

theorem Graph.IsVertexCover.exists_mem_inc {α : Type u} {β : Type v} {G : Graph α β} {C : Set ↑G.vertexSet} (hC : G.IsVertexCover C) (e : ↑G.edgeSet) : ∃ x ∈ C, G.Inc ↑e ↑x

Every actual edge is incident with a vertex of a vertex cover.

theorem Graph.IsVertexCover.subset {α : Type u} {β : Type v} {G : Graph α β} {C D : Set ↑G.vertexSet} (hC : G.IsVertexCover C) (hCD : C ⊆ D) : G.IsVertexCover D

A superset of a vertex cover is a vertex cover.

@[simp]

theorem Graph.isVertexCover_univ {α : Type u} {β : Type v} {G : Graph α β} : G.IsVertexCover Set.univ

The set of all actual vertices is a vertex cover.

@[simp]

theorem Graph.isVertexCover_empty_iff {α : Type u} {β : Type v} {G : Graph α β} : G.IsVertexCover ∅ ↔ G.edgeSet = ∅

The empty set is a vertex cover exactly when there are no actual edges.