finiteIndex_iInf — Mathlib

English

If ι is a finite index set and each f i has finite index, then the intersection over i of f i has finite index.

Русский

Если ι конечно, и для каждого i множество f i имеет конечный индекс, то пересечение по i имеет конечный индекс.

LaTeX

$$(⨅ i, f i).FiniteIndex$$

Lean4

@[to_additive]
theorem finiteIndex_iInf {ι : Type*} [Finite ι] {f : ι → Subgroup G} (hf : ∀ i, (f i).FiniteIndex) :
    (⨅ i, f i).FiniteIndex :=
  ⟨index_iInf_ne_zero fun i => (hf i).index_ne_zero⟩

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