English
The symmetry map of the order isomorphism sends a pair to the corresponding subgroup of H inside G.
Русский
Обратное от отображения порядок-изоморфизма сопоставляет соответствующую подгруппу H внутри G.
LaTeX
$$(\\text{MapSubtype}.orderIso H)^{-1}(sH') = sH'.1.subgroupOf H$$
Lean4
/-- Subgroups of the subgroup `H` are considered as subgroups that are less than or equal to
`H`. -/
@[to_additive (attr := simps apply_coe) /-- Additive subgroups of the subgroup `H` are considered as
additive subgroups that are less than or equal to `H`. -/
]
def orderIso (H : Subgroup G) : Subgroup ↥H ≃o { H' : Subgroup G // H' ≤ H }
where
toFun H' := ⟨H'.map H.subtype, map_subtype_le H'⟩
invFun sH' := sH'.1.subgroupOf H
left_inv H' := comap_map_eq_self_of_injective H.subtype_injective H'
right_inv sH' := Subtype.ext (map_subgroupOf_eq_of_le sH'.2)
map_rel_iff' := by simp
