sSup_ringCon — Mathlib

English

The supremum of a family of two-sided ideals has the same ring-con as the supremum of their ring-cons.

Русский

Наивысшее превосходство над семейством двусторонних идеалов сохраняет ringCon.

LaTeX

$$$\\forall S: Set\\ (TwoSidedIdeal R),\\ (sSup S).ringCon = sSup (TwoSidedIdeal.ringCon '' S).$$$

Lean4

theorem sSup_ringCon (S : Set (TwoSidedIdeal R)) : (sSup S).ringCon = sSup (TwoSidedIdeal.ringCon '' S) :=
  rfl

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