op_le_iff

Mathlib.Algebra.Algebra.Subalgebra.MulOpposite

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

English

For Subalgebra S1 ⊆ A and S2 ⊆ Aᵐᵒᵖ we have S1.op ≤ S2 ↔ S1 ≤ S2.unop.

Русский

Для подалгебр S1 ⊆ A и S2 ⊆ A^{op} выполняется S1^{op} ≤ S2 ↔ S1 ≤ S2.unop.

LaTeX

$$$ S_{1}^{\mathrm{op}} \le S_{2} \;\Leftrightarrow\; S_{1} \le S_{2}^{\mathrm{unop}}. $$$

Lean4

theorem op_le_iff {S₁ : Subalgebra R A} {S₂ : Subalgebra R Aᵐᵒᵖ} : S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop :=
  MulOpposite.op_surjective.forall

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

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

Разделы

Аффилиация

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