Theorems · Theorem · group theory

Subgroup.leftCoset_cover_filter_FiniteIndex_aux

∀ {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 →
    ∀ [inst_1 : DecidablePred Subgroup.FiniteIndex],
      ⋃ k ∈ {i ∈ s | (H i).FiniteIndex}, g k • ↑(H k) = Set.univ ∧
        1 ≤ ∑ i ∈ s, (↑(H i).index)⁻¹ ∧
          (∑ i ∈ s, (↑(H i).index)⁻¹ = 1 → (↑({i ∈ s | (H i).FiniteIndex})).PairwiseDisjoint fun i => g i • ↑(H i))

Defined in

Mathlib.GroupTheory.CosetCover

Cited by

3 results in Mathlib

Foundations

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

Assumes

GroupDecidablePred