English
If a finite cover of G by left cosets is given, one of the subgroups has index not exceeding the cover size.
Русский
Если конечное покрытие группы левых косет задано, то существует подгруппа с индексом не превышающим размер покрытия.
LaTeX
$$$\exists i \in s, (H i).FiniteIndex ∧ (H i).index ≤ |s|$$$
Lean4
/-- 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. -/
@[to_additive]
theorem exists_index_le_card_of_leftCoset_cover : ∃ i ∈ s, (H i).FiniteIndex ∧ (H i).index ≤ s.card :=
by
by_contra! h
apply (one_le_sum_inv_index_of_leftCoset_cover hcovers).not_gt
cases s.eq_empty_or_nonempty with
| inl hs => simp only [hs, Finset.sum_empty, zero_lt_one]
| inr hs =>
have hs' : 0 < s.card := hs.card_pos
have hlt : ∀ i ∈ s, ((H i).index : ℚ)⁻¹ < (s.card : ℚ)⁻¹ := fun i hi ↦ by
cases eq_or_ne (H i).index 0 with
| inl hindex => rwa [hindex, Nat.cast_zero, inv_zero, inv_pos, Nat.cast_pos]
| inr hindex => exact inv_strictAnti₀ (by exact_mod_cast hs') (by exact_mod_cast h i hi ⟨hindex⟩)
apply (Finset.sum_lt_sum_of_nonempty hs hlt).trans_eq
rw [Finset.sum_const, nsmul_eq_mul, mul_inv_cancel₀ (Nat.cast_ne_zero.mpr hs'.ne')]
