English
Let f: G1 →* G2 be a group homomorphism and let K be a subgroup of G2 with range(f) ≤ K. Then the subgroup of K generated by range(f) equals the range of the restricted map f|K.
Русский
Пусть f: G1 →* G2 — гомоморфизм групп, и K — подгруппа G2 такая, что изображение f лежит в K. Тогда подгруппа K, порождаемая изображением f, равна образу ограниченной карты f|K.
LaTeX
$$$$ \\operatorname{range}(f) \\subseteq K \\;\Longrightarrow\; \\operatorname{range}(f)\\,\\mathrm{subgroupOf}\\; K = \\operatorname{range}(f|_K) $$$$
Lean4
@[to_additive]
theorem subgroupOf_range_eq_of_le {G₁ G₂ : Type*} [Group G₁] [Group G₂] {K : Subgroup G₂} (f : G₁ →* G₂)
(h : f.range ≤ K) : f.range.subgroupOf K = (f.codRestrict K fun x => h ⟨x, rfl⟩).range :=
by
ext k
refine exists_congr ?_
simp [Subtype.ext_iff]
