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.