Kőnig's theorem

TheoremKőnig's theorem on a finite vertex type#✓fully proved

Let \(G\) be a bipartite simple graph on a finite vertex type \(V\). Then there are a matching \(M\) in \(G\) and a vertex cover \(C \subseteq V\) of \(G\) such that the number of edges of \(M\) equals the number of vertices in \(C\).

theorem konig_matching_cover_general {V : Type*} [Finite V] (G : SimpleGraph V)
    (hBip : G.IsBipartite) :
    ∃ (M : G.Subgraph) (C : Set V),
      M.IsMatching ∧ G.IsVertexCover C ∧ M.edgeSet.ncard = C.ncard

Used by 1

Used byKőnig's theorem for finite bipartite graphs

TheoremKőnig's theorem for finite bipartite graphs#✓fully proved

Every bipartite simple graph \(G\) on a finite vertex type \(V\) has a matching \(M\) and a vertex cover \(C \subseteq V\) such that the number of edges of \(M\) equals the number of vertices in \(C\).

@[nolint unusedArguments]
theorem konig_matching_cover {V : Type*} [Fintype V]
    [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj]
    (hBip : G.IsBipartite) :
    ∃ (M : G.Subgraph) (C : Set V),
      M.IsMatching ∧ G.IsVertexCover C ∧ M.edgeSet.ncard = C.ncard

Sources

• D. Kőnig (1931); J. Egerváry (1931) weighted form. It follows from konig_matching_cover_general; the instances [DecidableEq V] and [DecidableRel G.Adj] are unused and keep the source's shape.

Uses 1

Proof usesKőnig's theorem on a finite vertex type

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.