unop_sup

Mathlib.Algebra.Group.Submonoid.MulOpposite

URI: https://scilib.ai/kg/mathlib#Submonoid.unop_sup

English

Unop respects sup: (S1 ⊔ S2).unop = S1.unop ⊔ S2.unop.

Русский

Unop сохраняет объединение: (S1 ⊔ S2).unop = S1.unop ⊔ S2.unop.

LaTeX

$$$(S_1 \sqcup S_2)^{unop} = S_1^{unop} \sqcup S_2^{unop}$$$

Lean4

@[to_additive]
theorem unop_sup (S₁ S₂ : Submonoid Mᵐᵒᵖ) : (S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop :=
  opEquiv.symm.map_sup _ _

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

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

Разделы

Аффилиация

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