Hall's Marriage Theorem #
This file derives Hall's Marriage Theorem for bipartite graphs from the combinatorial formulation in
Mathlib/Combinatorics/Hall/Basic.lean.
Main statements #
exists_isMatching_of_forall_ncard_le: Hall's marriage theorem for a matching on a single partition of a bipartite graph.exists_isPerfectMatching_of_forall_ncard_le: Hall's marriage theorem for a perfect matching on a bipartite graph.
Tags #
Hall's Marriage Theorem
theorem SimpleGraph.exists_isMatching_of_forall_ncard_le {V : Type u_1} {G : SimpleGraph V} [G.LocallyFinite] {p₁ p₂ : Set V} (h₁ : G.IsBipartiteWith p₁ p₂) (h₂ : ∀ s ⊆ p₁, s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard) :
∃ (M : G.Subgraph), p₁ ⊆ M.verts ∧ M.IsMatching
This is the version of Hall's marriage theorem for bipartite graphs that finds a matching for a single partition given that the neighborhood-condition only holds for elements of that partition.
theorem SimpleGraph.union_eq_univ_of_forall_ncard_le {V : Type u_1} {G : SimpleGraph V} [G.LocallyFinite] {p₁ p₂ : Set V} (h₁ : G.IsBipartiteWith p₁ p₂) (h₂ : ∀ (s : Set V), s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard) :
theorem SimpleGraph.exists_bijective_of_forall_ncard_le {V : Type u_1} {G : SimpleGraph V} [G.LocallyFinite] {p₁ p₂ : Set V} (h₁ : G.IsBipartiteWith p₁ p₂) (h₂ : ∀ (s : Set V), s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard) :
∃ (h : ↑p₁ → ↑p₂), Function.Bijective h ∧ ∀ (a : ↑p₁), G.Adj ↑a ↑(h a)
theorem SimpleGraph.exists_isPerfectMatching_of_forall_ncard_le {V : Type u_1} {G : SimpleGraph V} [G.LocallyFinite] {p₁ p₂ : Set V} (h₁ : G.IsBipartiteWith p₁ p₂) (h₂ : ∀ (s : Set V), s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard) :
∃ (M : G.Subgraph), M.IsPerfectMatching
This is the version of Hall's marriage theorem for bipartite graphs that finds a perfect matching given that the neighborhood-condition holds globally.