English
Finitely generated subgroups can be characterized equivalently by a finite generating set S: FG(P) iff there exists a finite S with closure S equal to P.
Русский
Конечнопорожденная подгруппа эквивалентно существованию конечного множества порождающих S, для которого closure S = P.
LaTeX
$$$\text{FG}(P) \iff \exists S : Set G, Subgroup.closure S = P \land S.Finite$$$
Lean4
/-- An equivalent expression of `Subgroup.FG` in terms of `Set.Finite` instead of `Finset`. -/
@[to_additive /-- An equivalent expression of `AddSubgroup.fg` in terms of `Set.Finite` instead of
`Finset`. -/
]
theorem fg_iff (P : Subgroup G) : Subgroup.FG P ↔ ∃ S : Set G, Subgroup.closure S = P ∧ S.Finite :=
⟨fun ⟨S, hS⟩ => ⟨S, hS, Finset.finite_toSet S⟩, fun ⟨S, hS, hf⟩ => ⟨Set.Finite.toFinset hf, by simp [hS]⟩⟩
