unop_le_unop_iff

Mathlib.Algebra.Ring.Subsemiring.MulOpposite

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

English

For S1, S2 ⊆ R^op, S1.unop ≤ S2.unop iff S1 ≤ S2.

Русский

Для S1, S2 ⊆ R^op: S1.unop ≤ S2.unop ⇔ S1 ≤ S2.

LaTeX

$$$\forall {S1 S2 : \mathrm{Subsemiring}(R^{\mathrm{op}})}, S1.unop \le S2.unop \Leftrightarrow S1 \le S2$$$

Lean4

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

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

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

Разделы

Аффилиация

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