unop_iSup

Mathlib.Algebra.Ring.Subsemiring.MulOpposite

URI: https://scilib.ai/kg/mathlib#Subsemiring.unop_iSup

English

The unop of the directed supremum equals the directed supremum of the unops: (iSup S).unop = ⨆ i, (S i).unop.

Русский

Обратная к объединению по индексам равна объединению их обратных.

LaTeX

$$$ (\\mathrm{iSup} S)^{unop} = \\big\\lbrace (S(i))^{unop} \\rbrace_i $$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru