unop_iSup

Mathlib.Algebra.Algebra.Subalgebra.MulOpposite

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

English

The unop map takes iSup to the iSup of unops: (iSup S).unop = ⨆ i, (S i).unop.

Русский

Unop переводит iSup в iSup для unop: (iSup S).unop = ⨆ i, (S i).unop.

LaTeX

$$$$(\\mathrm{iSup}\\, S)^{unop} = \\big\\langle i, (S(i))^{unop} \\big\\rangle$$$$

Lean4

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

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

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

Разделы

Аффилиация

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