English
Let G be a group. Then G is finitely generated if and only if there exists a finite subset S of G such that the subgroup generated by S equals G.
Русский
Пусть G — группа. Тогда G конечно порождена тогда и только тогда, когда существует конечное подмножество S в G такое, что порождаемая им подгруппа равна всей G.
LaTeX
$$$\operatorname{FG}(G) \iff \exists S \subseteq G,\; |S| < \infty \land \operatorname{Subgroup.closure}(S) = \top$$$
Lean4
@[to_additive]
theorem fg_iff' : Group.FG G ↔ ∃ (n : _) (S : Finset G), S.card = n ∧ Subgroup.closure (S : Set G) = ⊤ :=
Group.fg_def.trans ⟨fun ⟨S, hS⟩ => ⟨S.card, S, rfl, hS⟩, fun ⟨_n, S, _hn, hS⟩ => ⟨S, hS⟩⟩
