The equality case of Hall's condition

For an indexed family of finite sets t : ι → Finset α, Hall's condition asks that #s ≤ #(s.biUnion t) for every s : Finset ι. This file studies the sets where that inequality is an equality, classically called tight or critical. The neighbourhood function s ↦ #(s.biUnion t) is submodular, so under Hall's condition the tight sets are closed under union and intersection.

Main results

• Finset.inter_biUnion_subset: (s ∩ u).biUnion t ⊆ s.biUnion t ∩ u.biUnion t.
• Finset.card_biUnion_union_add_card_biUnion_inter_le: submodularity.
• Finset.card_biUnion_union_eq_card_union, Finset.card_biUnion_inter_eq_card_inter: under Hall's condition, unions and intersections of tight sets are tight.

References

• L. Lovász, M. D. Plummer, Matching Theory, North-Holland, 1986, Chapter 1.

theorem Finset.inter_biUnion_subset {ι : Type u_1} {α : Type u_2} [DecidableEq ι] [DecidableEq α] (t : ι → Finset α) (s u : Finset ι) : (s ∩ u).biUnion t ⊆ s.biUnion t ∩ u.biUnion t

The neighbourhood of an intersection is contained in the intersection of the neighbourhoods. The reverse inclusion fails in general.

theorem Finset.card_biUnion_union_add_card_biUnion_inter_le {ι : Type u_1} {α : Type u_2} [DecidableEq ι] [DecidableEq α] (t : ι → Finset α) (s u : Finset ι) : ((s ∪ u).biUnion t).card + ((s ∩ u).biUnion t).card ≤ (s.biUnion t).card + (u.biUnion t).card

The neighbourhood function s ↦ #(s.biUnion t) of an indexed family of finite sets is submodular.

theorem Finset.card_biUnion_union_eq_card_union {ι : Type u_1} {α : Type u_2} [DecidableEq ι] [DecidableEq α] {t : ι → Finset α} {s u : Finset ι} (hall : ∀ (v : Finset ι), v.card ≤ (v.biUnion t).card) (hs : (s.biUnion t).card = s.card) (hu : (u.biUnion t).card = u.card) : ((s ∪ u).biUnion t).card = (s ∪ u).card

Under Hall's condition, the union of two tight sets is tight: if s and u both meet the Hall bound with equality, so does s ∪ u.

theorem Finset.card_biUnion_inter_eq_card_inter {ι : Type u_1} {α : Type u_2} [DecidableEq ι] [DecidableEq α] {t : ι → Finset α} {s u : Finset ι} (hall : ∀ (v : Finset ι), v.card ≤ (v.biUnion t).card) (hs : (s.biUnion t).card = s.card) (hu : (u.biUnion t).card = u.card) : ((s ∩ u).biUnion t).card = (s ∩ u).card

Under Hall's condition, the intersection of two tight sets is tight. Together with Finset.card_biUnion_union_eq_card_union, the tight sets form a sublattice.