English
If H ≤ K are subgroups of G, then the image of the natural inclusion i: H → K equals H viewed as a subgroup of K.
Русский
Если H ≤ K — подгруппы G, то образ естественного вложения i: H → K равен H, воспринятой как подгруппа K.
LaTeX
$$$$ \\mathrm{Im}(i_{H\\to K}) = H \\text{ (as a subgroup of } K) $$$$
Lean4
@[to_additive (attr := simp)]
theorem _root_.Subgroup.inclusion_range {H K : Subgroup G} (h_le : H ≤ K) : (inclusion h_le).range = H.subgroupOf K :=
Subgroup.ext fun g => Set.ext_iff.mp (Set.range_inclusion h_le) g