def HerzogSchonheim.IsCosetCover {G : Type u_1} [Group G] {ι : Type u_2} (s : Finset ι) (H : ι → Subgroup G) (g : ι → G) : Prop

A finite family of left cosets g i • H i that covers the whole group.

Equations

• HerzogSchonheim.IsCosetCover s H g = (⋃ i ∈ s, g i • ↑(H i) = Set.univ)

def HerzogSchonheim.IsDisjointCosetCover {G : Type u_1} [Group G] {ι : Type u_2} (s : Finset ι) (H : ι → Subgroup G) (g : ι → G) : Prop

A coset cover in which distinct listed cosets are pairwise disjoint.

Equations

• HerzogSchonheim.IsDisjointCosetCover s H g = (HerzogSchonheim.IsCosetCover s H g ∧ (↑s).PairwiseDisjoint fun (i : ι) => g i • ↑(H i))

def HerzogSchonheim.PairwiseDistinctIndices {G : Type u_1} [Group G] {ι : Type u_2} (s : Finset ι) (H : ι → Subgroup G) : Prop

The subgroup indices appearing in a finite family are pairwise distinct.

Equations

• HerzogSchonheim.PairwiseDistinctIndices s H = (↑s).Pairwise fun (i j : ι) => (H i).index ≠ (H j).index