English
If both a forward map f: G →* N and a backward map g: N →* G are mutual inverses on the level of sets, then mapping by f equals comapping by g on subgroups: map f H = comap g H.
Русский
Если f и g образуют взаимно обратные отображения на множестве, то отображение образа подгруппы через f совпадает с обратным образом подгруппы через g: map f H = comap g H.
LaTeX
$$$\\text{If } hl: g \\circ f = id \\,\\text{and } hr: f \\circ g = id, \\text{ then } \\operatorname{map} f H = \\operatorname{comap} g H$.$$
Lean4
@[to_additive]
theorem map_eq_comap_of_inverse {f : G →* N} {g : N →* G} (hl : Function.LeftInverse g f)
(hr : Function.RightInverse g f) (H : Subgroup G) : map f H = comap g H :=
SetLike.ext' <| by rw [coe_map, coe_comap, Set.image_eq_preimage_of_inverse hl hr]
