opEquiv — Mathlib

English

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

Русский

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

LaTeX

$$$Submonoid(M) \cong_o Submonoid(M^{op})$$$

Lean4

/-- A submonoid `H` of `G` determines a submonoid `H.op` of the opposite group `Gᵐᵒᵖ`. -/
@[to_additive (attr := simps) /-- A additive submonoid `H` of `G` determines an additive submonoid
    `H.op` of the opposite group `Gᵐᵒᵖ`. -/
    ]
def opEquiv : Submonoid M ≃o Submonoid Mᵐᵒᵖ where
  toFun := Submonoid.op
  invFun := Submonoid.unop
  left_inv := unop_op
  right_inv := op_unop
  map_rel_iff' := op_le_op_iff

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