relIndex_iInf_ne_zero — Mathlib

English

If each (f i).relIndex L ≠ 0 for a finite index family, then (⨅ i, f i).relIndex L ≠ 0.

Русский

Если для конечной семьи подгрупп каждый индекс не равен нулю, то их бесконечныйя пересечение имеет ненулевой индекс.

LaTeX

$$$\text{If } \forall i, (f_i).relIndex L \neq 0, \text{ then } (\bigwedge_i f_i).relIndex L \neq 0.$$$

Lean4

@[to_additive]
theorem relIndex_iInf_ne_zero {ι : Type*} [_hι : Finite ι] {f : ι → Subgroup G} (hf : ∀ i, (f i).relIndex L ≠ 0) :
    (⨅ i, f i).relIndex L ≠ 0 :=
  haveI := Fintype.ofFinite ι
  (Finset.prod_ne_zero_iff.mpr fun i _hi => hf i) ∘
    Nat.card_pi.symm.trans ∘ Finite.card_eq_zero_of_embedding (quotientiInfSubgroupOfEmbedding f L)

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