Theorems · Theorem · group theory

AddSubgroup.leftCoset_cover_filter_FiniteIndex_aux

∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_2} {H : ι → AddSubgroup G} {g : ι → G} {s : Finset ι},
  ⋃ i ∈ s, g i +ᵥ ↑(H i) = Set.univ →
    ∀ [inst_1 : DecidablePred AddSubgroup.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

AddGroupDecidablePred