unop_sup

Mathlib.Algebra.Ring.Subring.MulOpposite

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

English

The unop of the join equals the join of unops.

Русский

Unop от объединения равен объединению обстановок.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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