Theorems · Theorem · group theory

Subgroup.exists_index_le_card_of_leftCoset_cover

∀ {G : Type u_1} [inst : Group G] {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
  ⋃ i ∈ s, g i • ↑(H i) = Set.univ → ∃ i ∈ s, (H i).FiniteIndex ∧ (H i).index ≤ s.card

B. H. Neumann Lemma : If a finite family of cosets of subgroups covers the group, then at least one of these subgroups has index not exceeding the number of cosets.

Defined in

Mathlib.GroupTheory.CosetCover

Cited by

0 results in Mathlib

Foundations

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

Assumes

Group