English
Pulling back an opposite subgroup along the op map yields a subgroup of the original group: for H ≤ G^{op}, H^{unop} := { g ∈ G : g^{op} ∈ H } is a subgroup of G.
Русский
Взяв противоположную подгруппу H ≤ G^{op} и применив обратную операцию, получаем подгруппу H^{unop} ⊆ G, определяемую как { g ∈ G : g^{op} ∈ H }.
LaTeX
$$$H^{\mathrm{unop}} = \{ g \in G \mid g^{\mathrm{op}} \in H \} \\le G$$
Lean4
/-- Pull an opposite subgroup back to a subgroup along `MulOpposite.op` -/
@[to_additive (attr := simps) /--
Pull an opposite additive subgroup back to an additive subgroup along `AddOpposite.op` -/
]
protected def unop (H : Subgroup Gᵐᵒᵖ) : Subgroup G
where
carrier := MulOpposite.op ⁻¹' (H : Set Gᵐᵒᵖ)
one_mem' := H.one_mem
mul_mem' := fun ha hb => H.mul_mem hb ha
inv_mem' := H.inv_mem
