unop_iSup — Mathlib

English

Let S_i be a family of subrings of the opposite ring R^op. Then the unop of their supremum equals the supremum of their unops: (sup_i S_i).unop = sup_i (S_i.unop).

Русский

Пусть S_i — семейство подкольц кольца R в противоположном формате. Тогда Unop суммы (верхней грани) равен верхней грани унипс: (sup_i S_i).unop = sup_i (S_i.unop).

LaTeX

$$$(\sup_i S_i)^{\mathrm{unop}} = \sup_i \left(S_i^{\mathrm{unop}}\right)$$$

Lean4

theorem unop_iSup (S : ι → Subring Rᵐᵒᵖ) : (iSup S).unop = ⨆ i, (S i).unop :=
  opEquiv.symm.map_iSup _

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