Documentation

Linglib.Core.Combinatorics.SimpleGraph.MaximalIndepSet

Maximal independent sets of a finite graph #

[UPSTREAM] candidate for Mathlib/Combinatorics/SimpleGraph/Clique.lean. A set of vertices is a maximal independent set exactly when it is independent and every vertex outside it is adjacent to one inside. For a finset of vertices of a finite graph this is decidable, so the maximal independent sets form a computable finset.

Main definitions #

Main statements #

source
theorem SimpleGraph.maximal_isIndepSet_iff_forall_exists_adj {V : Type u_1} (G : SimpleGraph V) {s : Set V} :
Maximal G.IsIndepSet s ↔ G.IsIndepSet s ∧ ∀ v ∉ s, ∃ w ∈ s, G.Adj v w

A set of vertices is a maximal independent set exactly when it is independent and every vertex outside it is adjacent to one inside.

source
def SimpleGraph.maximalIndepSets {V : Type u_1} (G : SimpleGraph V) [Fintype V] [DecidableEq V] [DecidableRel G.Adj] :
Finset (Finset V)

The maximal independent sets of a finite graph.

Equations
  • G.maximalIndepSets = {s : Finset V | G.IsIndepSet ↑s ∧ ∀ v ∉ s, ∃ w ∈ s, G.Adj v w}
Instances For
    source
    @[simp]
    theorem SimpleGraph.mem_maximalIndepSets {V : Type u_1} (G : SimpleGraph V) [Fintype V] [DecidableEq V] [DecidableRel G.Adj] {s : Finset V} :
    s ∈ G.maximalIndepSets ↔ Maximal G.IsIndepSet ↑s