Berge's lemma

TheoremBerge's lemma for matching subgraphs#✓fully proved

Let \(G\) be a simple graph on a finite vertex set and let \(M\) be a matching subgraph of \(G\), so that every vertex of \(M\) is incident to exactly one edge of \(M\). Then \(M\) has the maximum number of edges among all matching subgraphs of \(G\) if and only if there is no \(M\)-augmenting path: a path in \(G\) of positive length between two distinct vertices \(u\) and \(v\), neither of which is a vertex of \(M\), whose consecutive edges alternate between edges of \(M\) and edges not in \(M\).

theorem berge_general {V : Type*} [Finite V] (G : SimpleGraph V)
    (M : G.Subgraph) (hM : M.IsMatching) :
    (∀ M' : G.Subgraph, M'.IsMatching → M'.edgeSet.ncard ≤ M.edgeSet.ncard) ↔
    ¬ ∃ (u v : V) (_ : u ≠ v) (p : G.Walk u v),
      p.support.Nodup ∧ u ∉ M.verts ∧ v ∉ M.verts ∧
        List.IsChain (fun e₁ e₂ => (e₁ ∈ M.edgeSet) ≠ (e₂ ∈ M.edgeSet)) p.edges ∧
        0 < p.length

Used by 1

Used byBerge's lemma

TheoremBerge's lemma#✓fully proved

Let \(G\) be a simple graph on a finite vertex set and let \(M\) be a matching of \(G\), that is, a finite set of edges of \(G\) no two distinct members of which share a vertex. Then \(M\) has maximum cardinality among all matchings of \(G\) if and only if there is no \(M\)-augmenting path: a path in \(G\) of positive length between two distinct vertices \(u\) and \(v\), neither of which lies on an edge of \(M\), whose consecutive edges alternate between edges of \(M\) and edges not in \(M\).

theorem Berge :
    ∀ {V : Type*} [Fintype V] (G : SimpleGraph V)
      (M : Finset (Sym2 V)),
      (∀ e ∈ M, e ∈ G.edgeSet) →
      (∀ e₁ ∈ M, ∀ e₂ ∈ M, e₁ ≠ e₂ → ∀ v : V, v ∈ e₁ → v ∉ e₂) →
      ((∀ (M' : Finset (Sym2 V)),
        (∀ e ∈ M', e ∈ G.edgeSet) →
        (∀ e₁ ∈ M', ∀ e₂ ∈ M', e₁ ≠ e₂ → ∀ v : V, v ∈ e₁ → v ∉ e₂) →
        M'.card ≤ M.card) ↔
      ¬ ∃ (u v : V) (_ : u ≠ v) (p : G.Walk u v),
        p.support.Nodup ∧ (∀ e ∈ M, u ∉ e) ∧ (∀ e ∈ M, v ∉ e) ∧
        List.IsChain (fun e₁ e₂ => (e₁ ∈ M) ≠ (e₂ ∈ M)) p.edges ∧ 0 < p.length)

Sources

• Wikipedia, Berge's theorem, https://en.wikipedia.org/wiki/Berge%27s_theorem.

Uses 1

Proof usesBerge's lemma for matching subgraphs

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.