index_iInf_le — Mathlib

English

For a finite family of subgroups, the index of the infimum is bounded below by the product of indices.

Русский

Для конечной семейства подгрупп индекс пересечения ограничен произведением индексов.

LaTeX

$$Для {G} [Group], {ι}, [Fintype ι], (f : ι → Subgroup G) → index(iInf f) ≥ product of indices$$

Lean4

@[to_additive]
theorem index_iInf_le {ι : Type*} [Fintype ι] (f : ι → Subgroup G) : (⨅ i, f i).index ≤ ∏ i, (f i).index := by
  simp_rw [← relIndex_top_right, relIndex_iInf_le]

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