index_iInf_ne_zero — Mathlib

English

If every index in a finite collection is nonzero, then the index of the infimum is nonzero.

Русский

Если у конечной коллекции индексов все ненулевые, то индекс пересечения тоже ненулевой.

LaTeX

$$For {ι : Type} [Finite ι] (f : ι → Subgroup G), (∀ i, (f i).relIndex L ≠ 0) → (iInf fun i => f i).relIndex L ≠ 0$$

Lean4

@[to_additive]
theorem index_iInf_ne_zero {ι : Type*} [Finite ι] {f : ι → Subgroup G} (hf : ∀ i, (f i).index ≠ 0) :
    (⨅ i, f i).index ≠ 0 := by
  simp_rw [← relIndex_top_right] at hf ⊢
  exact relIndex_iInf_ne_zero hf

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