Theorems · Theorem · combinatorics

SimpleGraph.exists_isMatching_of_forall_ncard_le

∀ {V : Type u_1} {G : SimpleGraph V} [G.LocallyFinite] {p₁ p₂ : Set V},
  G.IsBipartiteWith p₁ p₂ → (∀ s ⊆ p₁, s.ncard ≤ (⋃ x ∈ s, G.neighborSet x).ncard) → ∃ M, 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.

Defined in

Mathlib.Combinatorics.SimpleGraph.Hall

Cited by

0 results in Mathlib

Foundations

Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SimpleGraph.LocallyFinite