Lemma of B. H. Neumann on coverings of a group by cosets.

Let the group $G$ be the union of finitely many, let us say $n$, left cosets of subgroups $C₁$, $C₂$, ..., $Cₙ$: $$ G = ⋃_{i = 1}^n C_i g_i. $$

• Subgroup.exists_finiteIndex_of_leftCoset_cover at least one subgroup $C_i$ has finite index in $G$.

• Subgroup.leftCoset_cover_filter_FiniteIndex the cosets of subgroups of infinite index may be omitted from the covering.

• Subgroup.exists_index_le_card_of_leftCoset_cover : the index of (at least) one of these subgroups does not exceed $n$.

• Subgroup.one_le_sum_inv_index_of_leftCoset_cover : the sum of the inverses of the indexes of the $C_i$ is greater than or equal to 1.

• Subgroup.pairwiseDisjoint_leftCoset_cover_of_sum_inv_index_eq_one If the sum of the inverses of the indexes of the subgroups $C_i$ is equal to 1, then the cosets of the subgroups of finite index are pairwise disjoint.

A corollary of Subgroup.exists_finiteIndex_of_leftCoset_cover is:

• Subspace.union_ne_univ_of_lt_top : a vector space over an infinite field cannot be a finite union of proper subspaces.

This can be used to show that an algebraic extension of fields is determined by the set of all minimal polynomials (not proved here).

[1] [Neumann-1954], Groups Covered By Permutable Subsets, Lemma 4.1 [2] https://mathoverflow.net/a/17398/3332 [3] http://alpha.math.uga.edu/~pete/Neumann54.pdf

theorem AddSubgroup.exists_leftTransversal_of_FiniteIndex {G : Type u_1} [AddGroup G] {D : AddSubgroup G} {H : AddSubgroup G} [D.FiniteIndex] (hD_le_H : D ≤ H) : ∃ (t : Finset ↥H), ↑t ∈ AddSubgroup.leftTransversals ↑(D.addSubgroupOf H) ∧ ⋃ g ∈ t, ↑g +ᵥ ↑D = ↑H

abbrev AddSubgroup.exists_leftTransversal_of_FiniteIndex.match_1 {G : Type u_1} [AddGroup G] {D : AddSubgroup G} {H : AddSubgroup G} (motive : (∃ S ∈ AddSubgroup.leftTransversals ↑(D.addSubgroupOf H), 0 ∈ S) → Prop) : ∀ (x : ∃ S ∈ AddSubgroup.leftTransversals ↑(D.addSubgroupOf H), 0 ∈ S), (∀ (t : Set ↥H) (ht : t ∈ AddSubgroup.leftTransversals ↑(D.addSubgroupOf H) ∧ 0 ∈ t), motive ⋯) → motive x

Equations

• ⋯ = ⋯

theorem Subgroup.exists_leftTransversal_of_FiniteIndex {G : Type u_1} [Group G] {D : Subgroup G} {H : Subgroup G} [D.FiniteIndex] (hD_le_H : D ≤ H) : ∃ (t : Finset ↥H), ↑t ∈ Subgroup.leftTransversals ↑(D.subgroupOf H) ∧ ⋃ g ∈ t, ↑g • ↑D = ↑H

theorem AddSubgroup.leftCoset_cover_const_iff_surjOn {G : Type u_1} [AddGroup G] {ι : Type u_2} {s : Finset ι} {H : AddSubgroup G} {g : ι → G} : ⋃ i ∈ s, g i +ᵥ ↑H = Set.univ ↔ Set.SurjOn (fun (x : ι) => ↑(g x)) (↑s) Set.univ

theorem Subgroup.leftCoset_cover_const_iff_surjOn {G : Type u_1} [Group G] {ι : Type u_2} {s : Finset ι} {H : Subgroup G} {g : ι → G} : ⋃ i ∈ s, g i • ↑H = Set.univ ↔ Set.SurjOn (fun (x : ι) => ↑(g x)) (↑s) Set.univ

theorem AddSubgroup.finiteIndex_of_leftCoset_cover_const {G : Type u_1} [AddGroup G] {ι : Type u_2} {s : Finset ι} {H : AddSubgroup G} {g : ι → G} (hcovers : ⋃ i ∈ s, g i +ᵥ ↑H = Set.univ) : H.FiniteIndex

theorem Subgroup.finiteIndex_of_leftCoset_cover_const {G : Type u_1} [Group G] {ι : Type u_2} {s : Finset ι} {H : Subgroup G} {g : ι → G} (hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ) : H.FiniteIndex

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.

theorem AddSubgroup.index_le_of_leftCoset_cover_const {G : Type u_1} [AddGroup G] {ι : Type u_2} {s : Finset ι} {H : AddSubgroup G} {g : ι → G} (hcovers : ⋃ i ∈ s, g i +ᵥ ↑H = Set.univ) : H.index ≤ s.card

theorem Subgroup.index_le_of_leftCoset_cover_const {G : Type u_1} [Group G] {ι : Type u_2} {s : Finset ι} {H : Subgroup G} {g : ι → G} (hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ) : H.index ≤ s.card

theorem AddSubgroup.pairwiseDisjoint_leftCoset_cover_const_of_index_eq {G : Type u_1} [AddGroup G] {ι : Type u_2} {s : Finset ι} {H : AddSubgroup G} {g : ι → G} (hcovers : ⋃ i ∈ s, g i +ᵥ ↑H = Set.univ) (hind : H.index = s.card) : (↑s).PairwiseDisjoint fun (x : ι) => g x +ᵥ ↑H

theorem Subgroup.pairwiseDisjoint_leftCoset_cover_const_of_index_eq {G : Type u_1} [Group G] {ι : Type u_2} {s : Finset ι} {H : Subgroup G} {g : ι → G} (hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ) (hind : H.index = s.card) : (↑s).PairwiseDisjoint fun (x : ι) => g x • ↑H

abbrev AddSubgroup.exists_finiteIndex_of_leftCoset_cover_aux.match_1 {G : Type u_1} [AddGroup G] {ι : Type u_2} {H : ι → AddSubgroup G} {s : Finset ι} [DecidableEq (AddSubgroup G)] (motive : (∃ (a : ℕ), a = (Finset.image H s).card) → Prop) : ∀ (x : ∃ (a : ℕ), a = (Finset.image H s).card), (∀ (n : ℕ) (hn : n = (Finset.image H s).card), motive ⋯) → motive x

Equations

• ⋯ = ⋯

abbrev AddSubgroup.exists_finiteIndex_of_leftCoset_cover_aux.match_4 {G : Type u_3} [AddGroup G] [DecidableEq (AddSubgroup G)] {ι : Type u_2} {H : ι → AddSubgroup G} {s : Finset ι} (j : ι) : let κ := { x : ι // x ∈ Finset.filter (fun (x : ι) => H x ≠ H j) s } × Option { x : ι // x ∈ Finset.filter (fun (x : ι) => H x = H j) s }; (motive : κ → Sort u_1) → (x : κ) → ((k₁ : { x : ι // x ∈ Finset.filter (fun (x : ι) => H x ≠ H j) s }) → (k₂ : { x : ι // x ∈ Finset.filter (fun (x : ι) => H x = H j) s }) → motive (k₁, some k₂)) → ((k₁ : { x : ι // x ∈ Finset.filter (fun (x : ι) => H x ≠ H j) s }) → motive (k₁, none)) → motive x

Equations

• One or more equations did not get rendered due to their size.

abbrev AddSubgroup.exists_finiteIndex_of_leftCoset_cover_aux.match_9 {G : Type u_2} [AddGroup G] [DecidableEq (AddSubgroup G)] {ι : Type u_1} {H : ι → AddSubgroup G} {s : Finset ι} (j : ι) (K : { x : ι // x ∈ Finset.filter (fun (x : ι) => H x ≠ H j) s } × Option { x : ι // x ∈ Finset.filter (fun (x : ι) => H x = H j) s } → AddSubgroup G) (x : AddSubgroup G) : let κ := { x : ι // x ∈ Finset.filter (fun (x : ι) => H x ≠ H j) s } × Option { x : ι // x ∈ Finset.filter (fun (x : ι) => H x = H j) s }; ∀ (motive : (∃ (y : κ), K y = x) → Prop) (x_1 : ∃ (y : κ), K y = x), (∀ (k : κ) (hk : K k = x), motive ⋯) → motive x_1

Equations

• ⋯ = ⋯

abbrev AddSubgroup.exists_finiteIndex_of_leftCoset_cover_aux.match_7 {G : Type u_2} [AddGroup G] [DecidableEq (AddSubgroup G)] {ι : Type u_1} {H : ι → AddSubgroup G} {g : ι → G} {s : Finset ι} (j : ι) (y : G) (motive : (∃ (i : ι) (_ : i ∈ Finset.filter (fun (a : ι) => ¬H a = H j) s), y ∈ g i +ᵥ ↑(H i)) → Prop) : ∀ (x : ∃ (i : ι) (_ : i ∈ Finset.filter (fun (a : ι) => ¬H a = H j) s), y ∈ g i +ᵥ ↑(H i)), (∀ (i : ι) (hi : i ∈ Finset.filter (fun (a : ι) => ¬H a = H j) s) (hy : y ∈ g i +ᵥ ↑(H i)), motive ⋯) → motive x

Equations

• ⋯ = ⋯

abbrev AddSubgroup.exists_finiteIndex_of_leftCoset_cover_aux.match_10 {G : Type u_2} [AddGroup G] [DecidableEq (AddSubgroup G)] {ι : Type u_1} {H : ι → AddSubgroup G} {s : Finset ι} (j : ι) (K : { x : ι // x ∈ Finset.filter (fun (x : ι) => H x ≠ H j) s } × Option { x : ι // x ∈ Finset.filter (fun (x : ι) => H x = H j) s } → AddSubgroup G) (k : { x : ι // x ∈ Finset.filter (fun (x : ι) => H x ≠ H j) s } × Option { x : ι // x ∈ Finset.filter (fun (x : ι) => H x = H j) s }) : let κ := { x : ι // x ∈ Finset.filter (fun (x : ι) => H x ≠ H j) s } × Option { x : ι // x ∈ Finset.filter (fun (x : ι) => H x = H j) s }; ∀ (motive : (∃ i ∈ Finset.univ, K i ≠ K k ∧ (K i).FiniteIndex) → Prop) (x : ∃ i ∈ Finset.univ, K i ≠ K k ∧ (K i).FiniteIndex), (∀ (k' : κ) (hk' : k' ∈ Finset.univ ∧ K k' ≠ K k ∧ (K k').FiniteIndex), motive ⋯) → motive x

Equations

• ⋯ = ⋯

abbrev AddSubgroup.exists_finiteIndex_of_leftCoset_cover_aux.match_5 {G : Type u_2} [AddGroup G] [DecidableEq (AddSubgroup G)] {ι : Type u_1} {H : ι → AddSubgroup G} {g : ι → G} {s : Finset ι} (j : ι) (y : G) (motive : (∃ (i : ι) (_ : i ∈ Finset.filter (fun (x : ι) => H x = H j) s), y ∈ g i +ᵥ ↑(H i)) → Prop) : ∀ (x : ∃ (i : ι) (_ : i ∈ Finset.filter (fun (x : ι) => H x = H j) s), y ∈ g i +ᵥ ↑(H i)), (∀ (k : ι) (hk : k ∈ Finset.filter (fun (x : ι) => H x = H j) s) (hy : y ∈ g k +ᵥ ↑(H k)), motive ⋯) → motive x

Equations

• ⋯ = ⋯

abbrev AddSubgroup.exists_finiteIndex_of_leftCoset_cover_aux.match_2 {G : Type u_1} [AddGroup G] {ι : Type u_2} {H : ι → AddSubgroup G} {g : ι → G} {s : Finset ι} (j : ι) (motive : (∃ (x : G), ∀ i ∈ s, H i = H j → ↑(g i) ≠ ↑x) → Prop) : ∀ (x : ∃ (x : G), ∀ i ∈ s, H i = H j → ↑(g i) ≠ ↑x), (∀ (x : G) (hx : ∀ i ∈ s, H i = H j → ↑(g i) ≠ ↑x), motive ⋯) → motive x

Equations

• ⋯ = ⋯

abbrev AddSubgroup.exists_finiteIndex_of_leftCoset_cover_aux.match_6 {G : Type u_2} [AddGroup G] [DecidableEq (AddSubgroup G)] {ι : Type u_1} {H : ι → AddSubgroup G} {g : ι → G} {s : Finset ι} (j : ι) (x : G) (y : G) (k : ι) (motive : (∃ (i : ι) (_ : i ∈ Finset.filter (fun (x : ι) => H x ≠ H j) s), y ∈ g k + -x + g i +ᵥ ↑(H i)) → Prop) : ∀ (x_1 : ∃ (i : ι) (_ : i ∈ Finset.filter (fun (x : ι) => H x ≠ H j) s), y ∈ g k + -x + g i +ᵥ ↑(H i)), (∀ (i : ι) (hi : i ∈ Finset.filter (fun (x : ι) => H x ≠ H j) s) (hy : y ∈ g k + -x + g i +ᵥ ↑(H i)), motive ⋯) → motive x_1

Equations

• ⋯ = ⋯

theorem AddSubgroup.exists_finiteIndex_of_leftCoset_cover_aux {G : Type u_1} [AddGroup G] {ι : Type u_2} {H : ι → AddSubgroup G} {g : ι → G} {s : Finset ι} (hcovers : ⋃ i ∈ s, g i +ᵥ ↑(H i) = Set.univ) [DecidableEq (AddSubgroup G)] (j : ι) (hj : j ∈ s) (hcovers' : ⋃ i ∈ Finset.filter (fun (x : ι) => H x = H j) s, g i +ᵥ ↑(H i) ≠ Set.univ) : ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex

abbrev AddSubgroup.exists_finiteIndex_of_leftCoset_cover_aux.match_3 {G : Type u_2} [AddGroup G] {ι : Type u_1} {H : ι → AddSubgroup G} {g : ι → G} {s : Finset ι} (x : G) (y : G) ⦃z : G⦄ (motive : (∃ i ∈ s, x + (-y + z) ∈ g i +ᵥ ↑(H i)) → Prop) : ∀ (x_1 : ∃ i ∈ s, x + (-y + z) ∈ g i +ᵥ ↑(H i)), (∀ (i : ι) (hi : i ∈ s) (hmem : x + (-y + z) ∈ g i +ᵥ ↑(H i)), motive ⋯) → motive x_1

Equations

• ⋯ = ⋯

abbrev AddSubgroup.exists_finiteIndex_of_leftCoset_cover_aux.match_8 {G : Type u_2} [AddGroup G] [DecidableEq (AddSubgroup G)] {ι : Type u_1} {H : ι → AddSubgroup G} {s : Finset ι} (j : ι) : let κ := { x : ι // x ∈ Finset.filter (fun (x : ι) => H x ≠ H j) s } × Option { x : ι // x ∈ Finset.filter (fun (x : ι) => H x = H j) s }; ∀ (motive : Nonempty κ → Prop) (x : Nonempty κ), (∀ (k : κ), motive ⋯) → motive x

Equations

• ⋯ = ⋯

theorem Subgroup.exists_finiteIndex_of_leftCoset_cover_aux {G : Type u_1} [Group G] {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι} (hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ) [DecidableEq (Subgroup G)] (j : ι) (hj : j ∈ s) (hcovers' : ⋃ i ∈ Finset.filter (fun (x : ι) => H x = H j) s, g i • ↑(H i) ≠ Set.univ) : ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex

theorem AddSubgroup.exists_finiteIndex_of_leftCoset_cover {G : Type u_1} [AddGroup G] {ι : Type u_2} {H : ι → AddSubgroup G} {g : ι → G} {s : Finset ι} (hcovers : ⋃ i ∈ s, g i +ᵥ ↑(H i) = Set.univ) : ∃ k ∈ s, (H k).FiniteIndex

abbrev AddSubgroup.exists_finiteIndex_of_leftCoset_cover.match_1 {ι : Type u_1} {s : Finset ι} (motive : s.Nonempty → Prop) : ∀ (x : s.Nonempty), (∀ (j : ι) (hj : j ∈ s), motive ⋯) → motive x

Equations

• ⋯ = ⋯

abbrev AddSubgroup.exists_finiteIndex_of_leftCoset_cover.match_2 {G : Type u_2} [AddGroup G] {ι : Type u_1} {H : ι → AddSubgroup G} {s : Finset ι} (j : ι) (motive : (∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex) → Prop) : ∀ (x : ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex), (∀ (i : ι) (hi : i ∈ s) (left : H i ≠ H j) (hfi : (H i).FiniteIndex), motive ⋯) → motive x

Equations

• ⋯ = ⋯

theorem Subgroup.exists_finiteIndex_of_leftCoset_cover {G : Type u_1} [Group G] {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι} (hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ) : ∃ k ∈ s, (H k).FiniteIndex

Let the group G be the union of finitely many left cosets g i • H i. Then at least one subgroup H i has finite index in G.

abbrev AddSubgroup.leftCoset_cover_filter_FiniteIndex_aux.match_1 {G : Type u_1} [AddGroup G] {ι : Type u_2} {H : ι → AddSubgroup G} {s : Finset ι} (t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)) (j : ι) (hj : j ∈ s) (hjfi : (H j).FiniteIndex) (motive : (t j hj hjfi).Nonempty → Prop) : ∀ (x : (t j hj hjfi).Nonempty), (∀ (x : ↥(H j)) (hx : x ∈ t j hj hjfi), motive ⋯) → motive x

Equations

• ⋯ = ⋯

abbrev AddSubgroup.leftCoset_cover_filter_FiniteIndex_aux.match_3 {G : Type u_1} [AddGroup G] {ι : Type u_2} {H : ι → AddSubgroup G} {s : Finset ι} [DecidablePred AddSubgroup.FiniteIndex] (D : AddSubgroup G) (t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)) (K : (i : { x : ι // x ∈ s }) × { x : ↥(H ↑i) // x ∈ if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {0} } → AddSubgroup G) : let κ := (i : { x : ι // x ∈ s }) × { x : ↥(H ↑i) // x ∈ if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {0} }; ∀ (motive : (∃ (k : κ), (H ↑k.fst).FiniteIndex ∧ K k = D) → Prop) (x : ∃ (k : κ), (H ↑k.fst).FiniteIndex ∧ K k = D), (∀ (k : κ) (hkfi : (H ↑k.fst).FiniteIndex) (hk : K k = D), motive ⋯) → motive x

Equations

• ⋯ = ⋯

abbrev AddSubgroup.leftCoset_cover_filter_FiniteIndex_aux.match_5 {G : Type u_1} [AddGroup G] {ι : Type u_2} {H : ι → AddSubgroup G} {s : Finset ι} [DecidablePred AddSubgroup.FiniteIndex] (D : AddSubgroup G) (t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)) (f : (i : { x : ι // x ∈ s }) × { x : ↥(H ↑i) // x ∈ if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {0} } → G) (K : (i : { x : ι // x ∈ s }) × { x : ↥(H ↑i) // x ∈ if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {0} } → AddSubgroup G) ⦃i : ι⦄ ⦃x : G⦄ : let κ := (i : { x : ι // x ∈ s }) × { x : ↥(H ↑i) // x ∈ if h : (H ↑i).FiniteIndex then t ↑i ⋯ h else {0} }; ∀ (motive : (∃ (k : κ), ↑k.fst = i ∧ K k = D ∧ x ∈ f k +ᵥ ↑D) → Prop) (x_1 : ∃ (k : κ), ↑k.fst = i ∧ K k = D ∧ x ∈ f k +ᵥ ↑D), (∀ (k₁ : κ) (hik₁ : ↑k₁.fst = i) (hk₁ : K k₁ = D) (hxk₁ : x ∈ f k₁ +ᵥ ↑D), motive ⋯) → motive x_1

Equations

• ⋯ = ⋯

theorem AddSubgroup.leftCoset_cover_filter_FiniteIndex_aux {G : Type u_1} [AddGroup G] {ι : Type u_2} {H : ι → AddSubgroup G} {g : ι → G} {s : Finset ι} (hcovers : ⋃ i ∈ s, g i +ᵥ ↑(H i) = Set.univ) [DecidablePred AddSubgroup.FiniteIndex] : ⋃ k ∈ Finset.filter (fun (i : ι) => (H i).FiniteIndex) s, g k +ᵥ ↑(H k) = Set.univ ∧ 1 ≤ ∑ i ∈ s, (↑(H i).index)⁻¹ ∧ (∑ i ∈ s, (↑(H i).index)⁻¹ = 1 → (↑(Finset.filter (fun (i : ι) => (H i).FiniteIndex) s)).PairwiseDisjoint fun (i : ι) => g i +ᵥ ↑(H i))

abbrev AddSubgroup.leftCoset_cover_filter_FiniteIndex_aux.match_4 {G : Type u_1} [AddGroup G] {ι : Type u_2} {H : ι → AddSubgroup G} {g : ι → G} {s : Finset ι} (D : AddSubgroup G) (t : (i : ι) → i ∈ s → (H i).FiniteIndex → Finset ↥(H i)) ⦃x : G⦄ (i : ι) (hi : i ∈ s ∧ (H i).FiniteIndex) (motive : (∃ r ∈ t i ⋯ ⋯, x ∈ g i + ↑r +ᵥ ↑D) → Prop) : ∀ (this : ∃ r ∈ t i ⋯ ⋯, x ∈ g i + ↑r +ᵥ ↑D), (∀ (r : ↥(H i)) (hr : r ∈ t i ⋯ ⋯) (hxr : x ∈ g i + ↑r +ᵥ ↑D), motive ⋯) → motive this

Equations

• ⋯ = ⋯

abbrev AddSubgroup.leftCoset_cover_filter_FiniteIndex_aux.match_2 {G : Type u_2} [AddGroup G] {ι : Type u_1} {H : ι → AddSubgroup G} {s : Finset ι} (motive : (∃ k ∈ s, (H k).FiniteIndex) → Prop) : ∀ (x : ∃ k ∈ s, (H k).FiniteIndex), (∀ (j : ι) (hj : j ∈ s) (hjfi : (H j).FiniteIndex), motive ⋯) → motive x

Equations

• ⋯ = ⋯

theorem Subgroup.leftCoset_cover_filter_FiniteIndex_aux {G : Type u_1} [Group G] {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι} (hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ) [DecidablePred Subgroup.FiniteIndex] : ⋃ k ∈ Finset.filter (fun (i : ι) => (H i).FiniteIndex) s, g k • ↑(H k) = Set.univ ∧ 1 ≤ ∑ i ∈ s, (↑(H i).index)⁻¹ ∧ (∑ i ∈ s, (↑(H i).index)⁻¹ = 1 → (↑(Finset.filter (fun (i : ι) => (H i).FiniteIndex) s)).PairwiseDisjoint fun (i : ι) => g i • ↑(H i))

theorem AddSubgroup.leftCoset_cover_filter_FiniteIndex {G : Type u_1} [AddGroup G] {ι : Type u_2} {H : ι → AddSubgroup G} {g : ι → G} {s : Finset ι} (hcovers : ⋃ i ∈ s, g i +ᵥ ↑(H i) = Set.univ) [DecidablePred AddSubgroup.FiniteIndex] : ⋃ k ∈ Finset.filter (fun (i : ι) => (H i).FiniteIndex) s, g k +ᵥ ↑(H k) = Set.univ

theorem Subgroup.leftCoset_cover_filter_FiniteIndex {G : Type u_1} [Group G] {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι} (hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ) [DecidablePred Subgroup.FiniteIndex] : ⋃ k ∈ Finset.filter (fun (i : ι) => (H i).FiniteIndex) s, g k • ↑(H k) = Set.univ

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.

theorem AddSubgroup.one_le_sum_inv_index_of_leftCoset_cover {G : Type u_1} [AddGroup G] {ι : Type u_2} {H : ι → AddSubgroup G} {g : ι → G} {s : Finset ι} (hcovers : ⋃ i ∈ s, g i +ᵥ ↑(H i) = Set.univ) : 1 ≤ ∑ i ∈ s, (↑(H i).index)⁻¹

theorem Subgroup.one_le_sum_inv_index_of_leftCoset_cover {G : Type u_1} [Group G] {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι} (hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ) : 1 ≤ ∑ i ∈ s, (↑(H i).index)⁻¹

Let the group G be the union of finitely many left cosets g i • H i. Then the sum of the inverses of the indexes of the subgroups H i is greater than or equal to 1.

theorem AddSubgroup.pairwiseDisjoint_leftCoset_cover_of_sum_neg_index_eq_zero {G : Type u_1} [AddGroup G] {ι : Type u_2} {H : ι → AddSubgroup G} {g : ι → G} {s : Finset ι} (hcovers : ⋃ i ∈ s, g i +ᵥ ↑(H i) = Set.univ) [DecidablePred AddSubgroup.FiniteIndex] : ∑ i ∈ s, (↑(H i).index)⁻¹ = 1 → (↑(Finset.filter (fun (i : ι) => (H i).FiniteIndex) s)).PairwiseDisjoint fun (i : ι) => g i +ᵥ ↑(H i)

theorem Subgroup.pairwiseDisjoint_leftCoset_cover_of_sum_inv_index_eq_one {G : Type u_1} [Group G] {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι} (hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ) [DecidablePred Subgroup.FiniteIndex] : ∑ i ∈ s, (↑(H i).index)⁻¹ = 1 → (↑(Finset.filter (fun (i : ι) => (H i).FiniteIndex) s)).PairwiseDisjoint fun (i : ι) => g i • ↑(H i)

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.

theorem AddSubgroup.exists_index_le_card_of_leftCoset_cover {G : Type u_1} [AddGroup G] {ι : Type u_2} {H : ι → AddSubgroup G} {g : ι → G} {s : Finset ι} (hcovers : ⋃ i ∈ s, g i +ᵥ ↑(H i) = Set.univ) : ∃ i ∈ s, (H i).FiniteIndex ∧ (H i).index ≤ s.card

theorem Subgroup.exists_index_le_card_of_leftCoset_cover {G : Type u_1} [Group G] {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι} (hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ) : ∃ i ∈ s, (H i).FiniteIndex ∧ (H i).index ≤ s.card

B. H. Neumann Lemma : If a finite family of cosets of subgroups covers the group, then at least one of these subgroups has index not exceeding the number of cosets.

theorem Submodule.exists_finiteIndex_of_cover {R : Type u_1} {M : Type u_2} {ι : Type u_3} [Ring R] [AddCommGroup M] [Module R M] {p : ι → Submodule R M} {s : Finset ι} (hcovers : ⋃ i ∈ s, ↑(p i) = Set.univ) : ∃ k ∈ s, (p k).toAddSubgroup.FiniteIndex

theorem Subspace.biUnion_ne_univ_of_ne_top {k : Type u_1} {E : Type u_2} [DivisionRing k] [Infinite k] [AddCommGroup E] [Module k E] {s : Finset (Subspace k E)} (hs : ∀ p ∈ s, p ≠ ⊤) : ⋃ p ∈ s, ↑p ≠ Set.univ

theorem Subspace.exists_eq_top_of_biUnion_eq_univ {k : Type u_1} {E : Type u_2} [DivisionRing k] [Infinite k] [AddCommGroup E] [Module k E] {s : Finset (Subspace k E)} (hcovers : ⋃ p ∈ s, ↑p = Set.univ) : ∃ p ∈ s, p = ⊤