English
For a group G acting on a set α, the following are equivalent: the complement of the fixed set of every element of closure(S) is finite if and only if the same holds for every generator in S.
Русский
Для группы G, действующей на множество α, эквивалентны условия: дополнение множества фиксированных точек элемента из замыкания(S) конечно, если и только если тогда это верно для каждого генератора из S.
LaTeX
$$$\\Big(\\forall g \\in closure(S),\\ (fixedBy\\ α\\ g)^{c}.Finite\\Big) \\Leftrightarrow \\Big(\\forall g \\in S,\\ (fixedBy\\ α\\ g)^{c}.Finite\\Big$$$
Lean4
/-- If the support of each element in a generating set of a permutation group is finite,
then the support of every element in the group is finite. -/
theorem finite_compl_fixedBy_closure_iff {S : Set G} :
(∀ g ∈ closure S, (fixedBy α g)ᶜ.Finite) ↔ ∀ g ∈ S, (fixedBy α g)ᶜ.Finite :=
⟨fun h g hg ↦ h g (subset_closure hg), fun h g hg ↦
by
refine closure_induction h (by simp) (fun g g' _ _ hg hg' ↦ (hg.union hg').subset ?_) (by simp) hg
simp_rw [← compl_inter, compl_subset_compl, fixedBy_mul]⟩
