unop_iInf

Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas

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

English

The unop map commutes with iInf: the unop of the indexed infimum equals the infimum of the unops.

Русский

unop commute с iInf: (iInf S).unop = ⨅ i, (S i).unop.

LaTeX

$$$(\mathrm{iInf} S).unop = \bigsqcap_i (S_i)^{unop}$$$

Lean4

@[to_additive]
theorem unop_iInf (S : ι → Subgroup Gᵐᵒᵖ) : (iInf S).unop = ⨅ i, (S i).unop :=
  opEquiv.symm.map_iInf _

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

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

Разделы

Аффилиация

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