op_iSup

Mathlib.Algebra.Ring.Subring.MulOpposite

URI: https://scilib.ai/kg/mathlib#Subring.op_iSup

English

The op of the indexed supremum equals the indexed supremum of the ops.

Русский

Образ op у iSup равен iSup от образов.

LaTeX

$$$\bigl(\operatorname{iSup} S\bigr)^{op} = \operatorname{iSup} \bigl(i \mapsto (S(i))^{op}\bigr)$$$

Lean4

theorem op_iSup (S : ι → Subring R) : (iSup S).op = ⨆ i, (S i).op :=
  opEquiv.map_iSup _

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

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

Разделы

Аффилиация

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