Vertex cover

A vertex cover of a simple graph is a set of vertices such that every edge is incident to at least one of the vertices in the set.

Main definitions

• SimpleGraph.IsVertexCover G c: Predicate that c is a vertex cover of G.
• SimpleGraph.vertexCoverNum G: The vertex cover number, e.g. the size of a minimal vertex cover.

def SimpleGraph.IsVertexCover {V : Type u_1} (G : SimpleGraph V) (c : Set V) : Prop

c is a vertex cover of G if every edge in G is incident to at least one vertex in c.

Equations

• G.IsVertexCover c = ∀ ⦃v w : V⦄, G.Adj v w → v ∈ c ∨ w ∈ c

@[simp]

theorem SimpleGraph.isVertexCover_empty {V : Type u_1} {G : SimpleGraph V} : G.IsVertexCover ∅ ↔ G = ⊥

@[simp]

theorem SimpleGraph.isVertexCover_univ {V : Type u_1} {G : SimpleGraph V} : G.IsVertexCover Set.univ

@[simp]

theorem SimpleGraph.isVertexCover_bot {V : Type u_1} (c : Set V) : ⊥.IsVertexCover c

theorem SimpleGraph.IsVertexCover.subset {V : Type u_1} {G : SimpleGraph V} {c d : Set V} (hcd : c ⊆ d) (hc : G.IsVertexCover c) : G.IsVertexCover d

theorem SimpleGraph.IsVertexCover.mono {V : Type u_1} {G G' : SimpleGraph V} {c : Set V} (hG : G ≤ G') (hc : G'.IsVertexCover c) : G.IsVertexCover c

@[simp]

theorem SimpleGraph.isIndepSet_compl_iff_isVertexCover {V : Type u_1} {G : SimpleGraph V} {c : Set V} : G.IsIndepSet cᶜ ↔ G.IsVertexCover c

A set c is a vertex cover iff the complement of c is an independent set.

@[simp]

theorem SimpleGraph.isVertexCover_compl {V : Type u_1} {G : SimpleGraph V} {c : Set V} : G.IsVertexCover cᶜ ↔ G.IsIndepSet c

theorem SimpleGraph.IsVertexCover.preimage {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} {F : Type u_3} [FunLike F V W] [HomClass F G H] (f : F) {c : Set W} (hc : H.IsVertexCover c) : G.IsVertexCover (⇑f ⁻¹' c)

@[simp]

theorem SimpleGraph.isVertexCover_preimage_iso {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (f : G ≃g H) {c : Set W} : G.IsVertexCover (⇑f ⁻¹' c) ↔ H.IsVertexCover c

@[simp]

theorem SimpleGraph.isVertexCover_image_iso {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (f : G ≃g H) {c : Set V} : H.IsVertexCover (⇑f '' c) ↔ G.IsVertexCover c

noncomputable def SimpleGraph.vertexCoverNum {V : Type u_1} (G : SimpleGraph V) : ℕ∞

The vertex cover number of G is the minimal number of vertices in a vertex cover of G.

Equations

• G.vertexCoverNum = ⨅ (s : Set V), ⨅ (_ : G.IsVertexCover s), s.encard

theorem SimpleGraph.vertexCoverNum_le_iff {V : Type u_1} {G : SimpleGraph V} {n : ℕ∞} : G.vertexCoverNum ≤ n ↔ ∀ (m : ℕ∞), (∀ (s : Set V), G.IsVertexCover s → m ≤ s.encard) → m ≤ n

theorem SimpleGraph.IsVertexCover.vertexCoverNum_le {V : Type u_1} {G : SimpleGraph V} {c : Set V} (hc : G.IsVertexCover c) : G.vertexCoverNum ≤ c.encard

theorem SimpleGraph.vertexCoverNum_exists {V : Type u_1} (G : SimpleGraph V) : ∃ (s : Set V), s.encard = G.vertexCoverNum ∧ G.IsVertexCover s

theorem SimpleGraph.exists_of_le_vertexCoverNum {V : Type u_1} {G : SimpleGraph V} (n : ℕ) (h₁ : G.vertexCoverNum ≤ ↑n) (h₂ : ↑n ≤ ENat.card V) : ∃ (s : Set V), s.encard = ↑n ∧ G.IsVertexCover s

@[simp]

theorem SimpleGraph.vertexCoverNum_bot {V : Type u_1} : (emptyGraph V).vertexCoverNum = 0

@[simp]

theorem SimpleGraph.vertexCoverNum_of_subsingleton {V : Type u_1} {G : SimpleGraph V} [Subsingleton V] : G.vertexCoverNum = 0

@[simp]

theorem SimpleGraph.vertexCoverNum_eq_zero {V : Type u_1} {G : SimpleGraph V} : G.vertexCoverNum = 0 ↔ G = ⊥

theorem SimpleGraph.vertexCoverNum_le_card_sub_one {V : Type u_1} {G : SimpleGraph V} : G.vertexCoverNum ≤ ENat.card V - 1

@[simp]

theorem SimpleGraph.vertexCoverNum_ne_top_of_finite {V : Type u_1} {G : SimpleGraph V} [Finite V] : G.vertexCoverNum ≠ ⊤

theorem SimpleGraph.vertexCoverNum_lt_card {V : Type u_1} {G : SimpleGraph V} [Nonempty V] [Finite V] : G.vertexCoverNum < ENat.card V

theorem SimpleGraph.vertexCoverNum_le_encard_edgeSet {V : Type u_1} {G : SimpleGraph V} : G.vertexCoverNum ≤ G.edgeSet.encard

@[simp]

theorem SimpleGraph.vertexCoverNum_ne_top_of_finite_edgeSet {V : Type u_1} {G : SimpleGraph V} (h : G.edgeSet.Finite) : G.vertexCoverNum ≠ ⊤

@[simp]

theorem SimpleGraph.vertexCoverNum_top {V : Type u_1} : (completeGraph V).vertexCoverNum = ENat.card V - 1

theorem SimpleGraph.IsContained.vertexCoverNum_le_vertexCoverNum {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (h : G.IsContained H) : G.vertexCoverNum ≤ H.vertexCoverNum

@[deprecated SimpleGraph.IsContained.vertexCoverNum_le_vertexCoverNum (since := "2026-01-07")]

theorem SimpleGraph.vertexCoverNum_le_vertexCoverNum_of_injective {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (f : G →g H) (hf : Function.Injective ⇑f) : G.vertexCoverNum ≤ H.vertexCoverNum

theorem SimpleGraph.vertexCoverNum_mono {V : Type u_1} {G G' : SimpleGraph V} (h : G ≤ G') : G.vertexCoverNum ≤ G'.vertexCoverNum

theorem SimpleGraph.vertexCoverNum_congr {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} (f : G ≃g H) : G.vertexCoverNum = H.vertexCoverNum