English
An equivalent expression of Group.FG in terms of Set-Finite: Group.FG G is equivalent to the existence of a finite set S with closure S = ⊤.
Русский
Эквивалентное выражение Group.FG через множество: Group.FG G эквивалентно существованию конечного множества S с closure S = ⊤.
LaTeX
$$$\text{Group.FG } G \iff \exists S : Set G, Subgroup.closure S = \top \land S.Finite$$$
Lean4
/-- An equivalent expression of `Group.FG` in terms of `Set.Finite` instead of `Finset`. -/
@[to_additive /-- An equivalent expression of `AddGroup.fg` in terms of `Set.Finite` instead of `Finset`. -/
]
theorem fg_iff : Group.FG G ↔ ∃ S : Set G, Subgroup.closure S = (⊤ : Subgroup G) ∧ S.Finite :=
⟨fun h => (Subgroup.fg_iff ⊤).1 h.out, fun h => ⟨(Subgroup.fg_iff ⊤).2 h⟩⟩
