iSup_ringCon — Mathlib

English

Distributive property of ringCon with respect to directed suprema: (⨆ i, I_i).ringCon = ⨆ i, (I_i).ringCon.

Русский

Директированное взятие супремума и сохранение ringCon: (⨆ i, I_i).ringCon = ⨆ i, (I_i).ringCon.

LaTeX

$$$\\forall I: ι \\to TwoSidedIdeal\\; R,\\ (iSup fun i => I i).ringCon = iSup (fun i => (I i).ringCon).$$$

Lean4

theorem iSup_ringCon {ι : Type*} (I : ι → TwoSidedIdeal R) : (⨆ i, I i).ringCon = ⨆ i, (I i).ringCon := by
  simp only [iSup, sSup_ringCon]; congr; ext; simp

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