sInf_ringCon — Mathlib

English

The ring-construction congruence of the infimum over a set S of two-sided ideals equals the infimum of the ringCon images of S.

Русский

Конгруэнция кольцевой конструкции пересечения (inf) над множеством S двусторонних идеалов равна пересечению их образов через ringCon.

LaTeX

$$$(\\mathrm{sInf}\\, S).\\mathrm{ringCon} = \\mathrm{sInf}\\, (\\mathrm{ringCon}''\\, S)$$$

Lean4

theorem sInf_ringCon (S : Set (TwoSidedIdeal R)) : (sInf S).ringCon = sInf (TwoSidedIdeal.ringCon '' S) :=
  rfl

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