English
There is an order isomorphism between Subgroup G and Subgroup G^{op}, given by the correspondence H ↦ H^{op} with inverse H^{op} ↦ H.
Русский
Существует отображение сохранения порядка между подгруппами G и их противоположностями, задающее взаимно обратную связь H ↦ H^{op}.
LaTeX
$$Subgroup.opEquiv : Subgroup G ≃o Subgroup G^{\mathrm{op}}$$
Lean4
/-- A subgroup `H` of `G` determines a subgroup `H.op` of the opposite group `Gᵐᵒᵖ`. -/
@[to_additive (attr := simps) /-- An additive subgroup `H` of `G` determines an additive subgroup
`H.op` of the opposite additive group `Gᵃᵒᵖ`. -/
]
def opEquiv : Subgroup G ≃o Subgroup Gᵐᵒᵖ where
toFun := Subgroup.op
invFun := Subgroup.unop
left_inv := unop_op
right_inv := op_unop
map_rel_iff' := op_le_op_iff
