op_le_op_iff

Mathlib.Algebra.Ring.Subsemiring.MulOpposite

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

English

For Subsemirings S1, S2 of R, S1.op ≤ S2.op iff S1 ≤ S2.

Русский

Для подпSemiring S1, S2 ⊆ R, S1.op ≤ S2.op ⇔ S1 ≤ S2.

LaTeX

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

Lean4

@[simp]
theorem op_le_op_iff {S₁ S₂ : Subsemiring R} : S₁.op ≤ S₂.op ↔ S₁ ≤ S₂ :=
  MulOpposite.op_surjective.forall

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

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

Разделы

Аффилиация

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