le_op_iff

Mathlib.Algebra.Algebra.Subalgebra.MulOpposite

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

English

For Subalgebras S1 ⊆ Aᵐᵒᵖ and S2 ⊆ A, S1 ≤ S2.op ↔ S1.unop ≤ S2.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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