le_op_iff — Mathlib

English

Let R be a ring. For S1 a subring of the opposite ring R^op and S2 a subring of R, inclusion S1 ⊆ S2^{op} holds if and only if the unop of S1 is contained in S2.

Русский

Пусть R — кольцо. Пусть S1 — подкольцо противоложного кольца R^op, а S2 — подкольцо R. Тогда S1 ⊆ S2^{op} равносильно тому, что S1^{unop} ⊆ S2.

LaTeX

$$$S_1 \le S_2^{op} \iff S_1^{\mathrm{unop}} \le S_2$$$

Lean4

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

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