iInf_ringCon — Mathlib

English

For a family I i → TwoSidedIdeal R, the ringCon of the infimum equals the infimum of the ringCon of each member: (iInf I).ringCon = iInf (I i).ringCon.

Русский

Для семейства идеалов I i в кольце R выполняется равенство ringCon для пересечения по индексу: (iInf I).ringCon = iInf (I i).ringCon.

LaTeX

$$$(\\iInf i, I(i)).ringCon = \\iInf i, (I(i)).ringCon$$$

Lean4

theorem iInf_ringCon {ι : Type*} (I : ι → TwoSidedIdeal R) : (⨅ i, I i).ringCon = ⨅ i, (I i).ringCon := by
  simp only [iInf, sInf_ringCon]; congr!; ext; simp

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