unop_sup

Mathlib.Algebra.Ring.Subsemiring.MulOpposite

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

English

The unop of the join of S1 and S2 equals the join of their unops: (S1 ⊔ S2).unop = S1.unop ⊔ S2.unop.

Русский

Обратная от объединения S1 и S2 равна объединению их обратных.

LaTeX

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

Lean4

theorem unop_sup (S₁ S₂ : Subsemiring Rᵐᵒᵖ) : (S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop :=
  opEquiv.symm.map_sup _ _

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

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

Разделы

Аффилиация

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