le_op_iff

Mathlib.Algebra.Ring.Subsemiring.MulOpposite

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

English

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

Русский

Для S1 ⊆ R^op и S2 ⊆ R выполняется S1 ≤ S2.op ⇔ S1.unop ≤ S2.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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