pairwiseDisjoint_leftCoset_cover_of_sum_inv_index_eq_one

English

Under finite index hypotheses, there exists a left transversal for D in H with finite complement properties.

Русский

При конечном индексе существует левый транзверсал D в H с соответствующими свойствами дополнения.

LaTeX

$$$\exists t : Finset H, IsComplement (t : Set H) (D.subgroupOf H) ∧ ⋃ g ∈ t, (g : G) • (D : Set G) = H$$$

Lean4

/-- Let the group `G` be the union of finitely many left cosets `g i • H i`.
If the sum of the inverses of the indexes of the subgroups `H i` is equal to 1,
then the cosets of the subgroups of finite index are pairwise disjoint. -/
@[to_additive]
theorem pairwiseDisjoint_leftCoset_cover_of_sum_inv_index_eq_one [DecidablePred (FiniteIndex : Subgroup G → Prop)] :
    ∑ i ∈ s, ((H i).index : ℚ)⁻¹ = 1 →
      Set.PairwiseDisjoint (s.filter (fun i => (H i).FiniteIndex)) (fun i ↦ g i • (H i : Set G)) :=
  (leftCoset_cover_filter_FiniteIndex_aux hcovers).2.2

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