unop_le_unop_iff

Mathlib.Algebra.Algebra.Subalgebra.MulOpposite

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

English

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

Русский

Для S1, S2 ⊆ A^{op}, S1.unop ≤ S2.unop ↔ S1 ≤ S2.

LaTeX

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

Lean4

@[simp]
theorem unop_le_unop_iff {S₁ S₂ : Subalgebra R Aᵐᵒᵖ} : S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂ :=
  MulOpposite.unop_surjective.forall

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

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

Разделы

Аффилиация

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