unop_iSup

Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas

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

English

The unop map commutes with iSup: the unop of the indexed supremum equals the supremum of the unops.

Русский

unop commute с iSup: (iSup S).unop = ⨆ i, (S i).unop.

LaTeX

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

Lean4

@[to_additive]
theorem unop_iSup (S : ι → Subgroup Gᵐᵒᵖ) : (iSup S).unop = ⨆ i, (S i).unop :=
  opEquiv.symm.map_iSup _

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

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

Разделы

Аффилиация

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