finiteIndex_of_leftCoset_cover_const

English

If a finite family of left cosets of subgroups covers a group, then some subgroup in the family has finite index.

Русский

Если конечная семья левых косет подгрупп покрывает группу, то в семье найдётся подгруппа с конечным индексом.

LaTeX

$$$\exists k \in s, (H k).FiniteIndex$$$

Lean4

/-- If `H` is a subgroup of `G` and `G` is the union of a finite family of left cosets of `H`
then `H` has finite index. -/
@[to_additive]
theorem finiteIndex_of_leftCoset_cover_const : H.FiniteIndex :=
  by
  simp_rw [leftCoset_cover_const_iff_surjOn] at hcovers
  have := Set.finite_univ_iff.mp <| Set.Finite.of_surjOn _ hcovers s.finite_toSet
  exact H.finiteIndex_of_finite_quotient

Похожие утверждения