theorem HerzogSchonheim.IsDisjointCosetCover.isCosetCover {G : Type u_1} [Group G] {ι : Type u_2} {s : Finset ι} {H : ι → Subgroup G} {g : ι → G} (h : IsDisjointCosetCover s H g) : IsCosetCover s H g

theorem HerzogSchonheim.not_isCosetCover_empty {G : Type u_1} [Group G] {ι : Type u_2} (H : ι → Subgroup G) (g : ι → G) : ¬IsCosetCover ∅ H g

theorem HerzogSchonheim.IsCosetCover.nonempty {G : Type u_1} [Group G] {ι : Type u_2} {s : Finset ι} {H : ι → Subgroup G} {g : ι → G} (h : IsCosetCover s H g) : s.Nonempty

Every coset cover uses at least one listed coset.

theorem HerzogSchonheim.exists_finiteIndex_and_le_card_of_isCosetCover {G : Type u_1} [Group G] {ι : Type u_2} (s : Finset ι) (H : ι → Subgroup G) (g : ι → G) (hcover : IsCosetCover s H g) : ∃ i ∈ s, (H i).FiniteIndex ∧ (H i).index ≤ s.card

Neumann's index bound, packaged in the local project vocabulary.

theorem HerzogSchonheim.exists_finiteIndex_and_le_card_of_isDisjointCosetCover {G : Type u_1} [Group G] {ι : Type u_2} (s : Finset ι) (H : ι → Subgroup G) (g : ι → G) (hcover : IsDisjointCosetCover s H g) : ∃ i ∈ s, (H i).FiniteIndex ∧ (H i).index ≤ s.card

theorem HerzogSchonheim.one_le_sum_inv_index_of_isCosetCover {G : Type u_1} [Group G] {ι : Type u_2} (s : Finset ι) (H : ι → Subgroup G) (g : ι → G) (hcover : IsCosetCover s H g) : 1 ≤ ∑ i ∈ s, (↑(H i).index)⁻¹

Sum-of-reciprocals lower bound from Neumann's coset-cover lemma.

theorem HerzogSchonheim.one_le_sum_inv_index_of_isDisjointCosetCover {G : Type u_1} [Group G] {ι : Type u_2} (s : Finset ι) (H : ι → Subgroup G) (g : ι → G) (hcover : IsDisjointCosetCover s H g) : 1 ≤ ∑ i ∈ s, (↑(H i).index)⁻¹