unop_inf

Mathlib.Algebra.Algebra.Subalgebra.MulOpposite

URI: https://scilib.ai/kg/mathlib#Subalgebra.unop_inf

English

For subalgebras of Aᵐᵒᵖ, unop preserves infimum: (S1 ⊓ S2).unop = S1.unop ⊓ S2.unop.

Русский

Для подалгебр Aᵐᵒᵖ операция unop сохраняет пересечение: (S1 ⊓ S2).unop = S1.unop ⊓ S2.unop.

LaTeX

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

Lean4

theorem unop_inf (S₁ S₂ : Subalgebra R Aᵐᵒᵖ) : (S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop :=
  opEquiv.symm.map_inf _ _

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

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

Разделы

Аффилиация

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