op_iSup

Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas

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

English

Opposite commutes with indexed sup: the op of the iSup equals the iSup of the opposites.

Русский

Противоположная операция commute с iSup: (iSup S).op = ⨆ i, (S i).op.

LaTeX

$$$(\mathrm{iSup} S).op = \bigsqcup_i (S_i)^{op}$$$

Lean4

@[to_additive]
theorem op_iSup (S : ι → Subgroup G) : (iSup S).op = ⨆ i, (S i).op :=
  opEquiv.map_iSup _

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

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

Разделы

Аффилиация

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