finiteIndex_iInf' — Mathlib

English

For a finite set s of indices, if each f i has finite index for i in s, then the infimum over i in s of f i has finite index.

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem finiteIndex_iInf' {ι : Type*} {s : Finset ι} (f : ι → Subgroup G) (hs : ∀ i ∈ s, (f i).FiniteIndex) :
    (⨅ i ∈ s, f i).FiniteIndex := by
  rw [iInf_subtype']
  exact finiteIndex_iInf fun ⟨i, hi⟩ => hs i hi

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