English
If a subgroup H of the presented group contains all images of the generators, then H contains every element of the presented group.
Русский
Если подгруппа H представленной группы содержит все образы генераторов, то она содержит и всякую величину группы.
LaTeX
$$If $H$ is a subgroup of $\mathrm{PresentedGroup}(\mathrm{rels})$ and $\mathrm{of}(j)\in H$ for all $j\in \alpha$, then $H = \mathrm{PresentedGroup}(\mathrm{rels})$.$$
Lean4
theorem generated_by (rels : Set (FreeGroup α)) (H : Subgroup (PresentedGroup rels))
(h : ∀ j : α, PresentedGroup.of j ∈ H) (x : PresentedGroup rels) : x ∈ H :=
by
obtain ⟨z⟩ := x
induction z
· exact one_mem H
· exact h _
· exact (Subgroup.inv_mem_iff H).mpr (by assumption)
rename_i h1 h2
change QuotientGroup.mk _ ∈ H.carrier
rw [QuotientGroup.mk_mul]
exact Subgroup.mul_mem _ h1 h2
