op_iSup — Mathlib

English

The op map takes the iSup of a family of subalgebras to the iSup of their opposites: (iSup S).op = ⨆ i, (S i).op.

Русский

Операция опеределяет отображение iSup семейства подалгебр в iSup их противоположностей: (iSup S).op = ⨆ i, (S i).op.

LaTeX

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

Lean4

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

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