leftCoset_cover_filter_FiniteIndex

English

A refined auxiliary lemma that packages the finite-index coset cover into a two-part statement: existence of a finite subcover and a density bound.

Русский

Уточняющая вспомогательная лемма, формулирующая существование конечного подпокрытия и ограничение плотности.

LaTeX

$$(see formal statement in code)$$

Lean4

/-- Let the group `G` be the union of finitely many left cosets `g i • H i`.
Then the cosets of subgroups of infinite index may be omitted from the covering. -/
@[to_additive]
theorem leftCoset_cover_filter_FiniteIndex [DecidablePred (FiniteIndex : Subgroup G → Prop)] :
    ⋃ k ∈ s.filter (fun i => (H i).FiniteIndex), g k • (H k : Set G) = Set.univ :=
  (leftCoset_cover_filter_FiniteIndex_aux hcovers).1

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