op_le_iff — Mathlib

English

There exists an order isomorphism between Submonoid M and Submonoid Mᵐᵒᵖ given by op and unop.

Русский

Между подмонойдами M и Mᵐᵒᵖ существует порядковый изоморфизм, заданный операцией оп/обратно.

LaTeX

$$$Submonoid(M) \cong_o Submonoid(M^{\mathrm{op}})$, via $S \mapsto S^{op}$ and $T \mapsto T^{unop}$.$$

Lean4

@[to_additive]
theorem op_le_iff {S₁ : Submonoid M} {S₂ : Submonoid Mᵐᵒᵖ} : S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop :=
  MulOpposite.op_surjective.forall

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