def WList.pathCover {α : Type u_1} {β : Type u_2} : WList α β → Set α

Equations

• (WList.nil u).pathCover = ∅
• (WList.cons u e (WList.nil v)).pathCover = {v}
• (WList.cons u e (WList.cons v e_1 w)).pathCover = insert v w.pathCover

theorem WList.pathCover_subset {α : Type u_1} {β : Type u_2} (P : WList α β) : P.pathCover ⊆ P.vertexSet

theorem WList.pathCover_inc {α : Type u_1} {β : Type u_2} {e : β} {P : WList α β} (hw : P.WellFormed) (he : e ∈ P.edgeSet) : e ∈ E(P.toGraph, P.pathCover)

theorem WList.pathCover_isCover {α : Type u_1} {β : Type u_2} {P : WList α β} (hw : P.WellFormed) : P.toGraph.IsCover P.pathCover

theorem WList.pathCover_ncard {α : Type u_1} {β : Type u_2} {P : WList α β} (hw : P.vertex.Nodup) : P.pathCover.ncard = P.vertexSet.ncard / 2

def WList.pathMatching {α : Type u_1} {β : Type u_2} : WList α β → Set β

Equations

• (WList.nil u).pathMatching = ∅
• (WList.cons u e (WList.nil v)).pathMatching = {e}
• (WList.cons u e (WList.cons v e_1 w)).pathMatching = insert e w.pathMatching

theorem WList.pathMatching_subset {α : Type u_1} {β : Type u_2} (P : WList α β) : P.pathMatching ⊆ P.edgeSet

theorem WList.toGraph_cons_addEdge {α : Type u_1} {β : Type u_2} {u : α} {e : β} {w : WList α β} (h : (cons u e w).WellFormed) : (cons u e w).toGraph = w.toGraph.addEdge e u w.first

theorem Graph.addEdge_isLink_iff' {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {e f : β} {a b : α} : (G.addEdge e a b).IsLink f x y ↔ f = e ∧ s(a, b) = s(x, y) ∨ f ≠ e ∧ G.IsLink f x y

theorem Graph.addEdge_inc_self_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {u x y : α} {e : β} : (G.addEdge e x y).Inc e u ↔ u = x ∨ u = y

@[simp]

theorem Graph.addEdge_inc_left {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {e : β} : (G.addEdge e x y).Inc e x

@[simp]

theorem Graph.addEdge_inc_right {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {e : β} : (G.addEdge e x y).Inc e y

theorem Graph.addEdge_inc_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {u x y : α} {e f : β} : (G.addEdge e x y).Inc f u ↔ f = e ∧ (u = x ∨ u = y) ∨ f ≠ e ∧ G.Inc f u

theorem Graph.addEdge_restrict_commutes {α : Type u_1} {β : Type u_2} {G : Graph α β} {M : Set β} {x y : α} {e : β} : (G.addEdge e x y).restrict (insert e M) = (G.restrict M).addEdge e x y

@[simp]

theorem Graph.restrict_eDegree_le_eDegree {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} {F : Set β} : (G.restrict F).eDegree x ≤ G.eDegree x

@[simp]

theorem Graph.ENat.le_zero {i : ℕ∞} : i ≤ 0 ↔ i = 0

theorem Graph.mem_edgeSet_iff_exists_inc {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} : e ∈ G.edgeSet ↔ ∃ (x : α), G.Inc e x

theorem Graph.Compatible.union_incEdges_eq {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G.Compatible H) (x : α) : E(G ∪ H, x) = E(G, x) ∪ E(H, x)

theorem Graph.union_incEdges_eq {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hdj : Disjoint G.edgeSet H.edgeSet) (x : α) : E(G ∪ H, x) = E(G, x) ∪ E(H, x)

@[simp]

theorem Graph.singleEdge_incEdges_left {α : Type u_1} {β : Type u_2} (x y : α) (e : β) : E(Graph.singleEdge x y e, x) = {e}

@[simp]

theorem Graph.singleEdge_incEdges_right {α : Type u_1} {β : Type u_2} (x y : α) (e : β) : E(Graph.singleEdge x y e, y) = {e}

@[simp]

theorem Graph.singleEdge_incEdges_of_ne {α : Type u_1} {β : Type u_2} {u x y : α} (e : β) (hux : u ≠ x) (huy : u ≠ y) : E(Graph.singleEdge x y e, u) = ∅

@[simp]

theorem Graph.singleEdge_incEdges_encard_left {α : Type u_1} {β : Type u_2} (x y : α) (e : β) : E(Graph.singleEdge x y e, x).encard = 1

@[simp]

theorem Graph.singleEdge_incEdges_encard_right {α : Type u_1} {β : Type u_2} (x y : α) (e : β) : E(Graph.singleEdge x y e, y).encard = 1

@[simp]

theorem Graph.singleEdge_incEdges_encard_of_ne {α : Type u_1} {β : Type u_2} {u x y : α} (e : β) (hux : u ≠ x) (huy : u ≠ y) : E(Graph.singleEdge x y e, u).encard = 0

@[simp]

theorem Graph.addEdge_incEdges_left {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} (he : e ∉ G.edgeSet) (x y : α) : E(G.addEdge e x y, x) = insert e E(G, x)

@[simp]

theorem Graph.addEdge_incEdges_right {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} (he : e ∉ G.edgeSet) (x y : α) : E(G.addEdge e x y, y) = insert e E(G, y)

@[simp]

theorem Graph.addEdge_incEdges_of_ne {α : Type u_1} {β : Type u_2} {G : Graph α β} {u x y : α} {e : β} (he : e ∉ G.edgeSet) (hux : u ≠ x) (huy : u ≠ y) : E(G.addEdge e x y, u) = E(G, u)

@[simp]

theorem Graph.addEdge_incEdges_encard_left {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} (he : e ∉ G.edgeSet) (x y : α) : E(G.addEdge e x y, x).encard = E(G, x).encard + 1

@[simp]

theorem Graph.addEdge_incEdges_encard_right {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} (he : e ∉ G.edgeSet) (x y : α) : E(G.addEdge e x y, y).encard = E(G, y).encard + 1

@[simp]

theorem Graph.addEdge_incEdges_encard_of_ne {α : Type u_1} {β : Type u_2} {G : Graph α β} {u x y : α} {e : β} (he : e ∉ G.edgeSet) (hux : u ≠ x) (huy : u ≠ y) : E(G.addEdge e x y, u).encard = E(G, u).encard

@[simp]

theorem Graph.incEdges_encard_mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hle : G ≤ H) (x : α) : E(G, x).encard ≤ E(H, x).encard

@[simp]

theorem Graph.restrict_incEdges_encard_le_encard {α : Type u_1} {β : Type u_2} {G : Graph α β} (F : Set β) (x : α) : E(G.restrict F, x).encard ≤ E(G, x).encard

@[simp]

theorem Graph.incEdges_addEdge_of_notMem_left {α : Type u_1} {β : Type u_2} {G : Graph α β} (e : β) (x y : α) (hx : x ∉ G.vertexSet) : E(G.addEdge e x y, x) = {e}

@[simp]

theorem Graph.incEdges_addEdge_of_notMem_right {α : Type u_1} {β : Type u_2} {G : Graph α β} (e : β) (x y : α) (hy : y ∉ G.vertexSet) : E(G.addEdge e x y, y) = {e}

theorem Graph.IsPath.pathMatching_isMatching {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (hP : G.IsPath P) : P.toGraph.IsMatching P.pathMatching

theorem Graph.pathMatching_ncard {α : Type u_1} {β : Type u_2} {P : WList α β} (hvertex_nodup : P.vertex.Nodup) (hedge_nodup : P.edge.Nodup) : P.pathMatching.ncard = P.vertexSet.ncard / 2

theorem Graph.IsPathGraph.konig {α : Type u_1} {β : Type u_2} {G : Graph α β} (h : G.IsPathGraph) : G.coverNumber = G.matchingNumber

theorem Graph.pathCover_odd {α : Type u_1} {β : Type u_2} {w : WList α β} (h : Odd w.length) : w.last ∈ w.pathCover

theorem Graph.IsCycle.konig {α : Type u_1} {β : Type u_2} {G : Graph α β} (hB : G.Bipartite) (h : G.IsCycle) : G.coverNumber = G.matchingNumber

König's Matching Theorem

Source: Romeo Rizzi (2000) [cite: 2]

Theorem: Let G be a bipartite graph. Then ν(G) = τ(G).

Proof: Let G be a minimal counterexample. Then G is connected, is not a circuit, nor a path. [cite: 14] So, G has a node of degree at least 3. Let u be such a node and v one of its neighbors. [cite: 15]

Case 1: If ν(G \ v) < ν(G). [cite: 16] By minimality, G \ v has a cover W' with |W'| < ν(G). [cite: 16] Hence, W' ∪ {v} is a cover of G with cardinality ν(G) at most. [cite: 17]

Case 2: Assume there exists a maximum matching M of G having no edge incident at v. [cite: 18] Let f be an edge of G \ M incident at u but not at v. [cite: 18] Let W' be a cover of G \ f with |W'| = ν(G). [cite: 22] Since no edge of M is incident at v, it follows that W' does not contain v. [cite: 22] So W' contains u and is a cover of G. [cite: 22]

theorem Graph.Konig'sTheorem {α : Type u_1} {β : Type u_2} {H : Graph α β} [H.Simple] [H.Finite] (hB : H.Bipartite) : H.coverNumber = H.matchingNumber