instIsTwoSidedIInf — Mathlib

English

The infimum of any family of two-sided ideals is two-sided.

Русский

Первообразение пересечения двухсторонних идеалов сохраняет свойство двусторонности.

LaTeX

$$$IsTwoSided(\\\\mathrm{iInf} \\\\, I) \\\\text{ for } I(i) \\\\text{ with } (I(i)).IsTwoSided$$$

Lean4

instance (priority := low) {ι} (I : ι → Ideal α) [∀ i, (I i).IsTwoSided] : (⨅ i, I i).IsTwoSided :=
  ⟨fun _ h ↦ (Submodule.mem_iInf _).mpr (mul_mem_right _ _ <| (Submodule.mem_iInf _).mp h ·)⟩

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