op_le_iff — Mathlib

English

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

Русский

Для подпSemiring S1 ⊆ R и S2 ⊆ R^op имеет место S1.op ≤ S2 ⇔ S1 ≤ S2.unop.

LaTeX

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

Lean4

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

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