English
From a left-coset cover of G, there is a k ∈ s with (H_k) having finite index.
Русский
Из покрытия левых косет следует существование k ∈ s такая, что H_k имеет конечный индекс.
LaTeX
$$$\exists k \in s, (H k).FiniteIndex$$$
Lean4
/-- Let the group `G` be the union of finitely many left cosets `g i • H i`.
Then at least one subgroup `H i` has finite index in `G`. -/
@[to_additive]
theorem exists_finiteIndex_of_leftCoset_cover : ∃ k ∈ s, (H k).FiniteIndex := by
classical
have ⟨j, hj⟩ : s.Nonempty :=
Finset.nonempty_iff_ne_empty.mpr fun hempty =>
by
rw [hempty, ← Finset.set_biUnion_coe, Finset.coe_empty, Set.biUnion_empty] at hcovers
exact Set.empty_ne_univ hcovers
by_cases hcovers' : ⋃ i ∈ s.filter (H · = H j), g i • (H i : Set G) = Set.univ
· rw [Set.iUnion₂_congr fun i hi => by rw [(Finset.mem_filter.mp hi).right]] at hcovers'
exact ⟨j, hj, finiteIndex_of_leftCoset_cover_const hcovers'⟩
· have ⟨i, hi, _, hfi⟩ := exists_finiteIndex_of_leftCoset_cover_aux hcovers j hj hcovers'
exact
⟨i, hi, hfi⟩
-- Auxiliary to `leftCoset_cover_filter_FiniteIndex` and `one_le_sum_inv_index_of_leftCoset_cover`.
