English
Let G act on α. For any a ∈ G and any subset s ⊆ α, a belongs to the stabilizer of s if and only if for every element b ∈ α, a · b ∈ s iff b ∈ s.
Русский
Пусть G действует на α. Пусть a ∈ G и s ⊆ α. Тогда a принадлежит стабилизатору множества s тогда и только тогда, когда для каждого b ∈ α верно: a · b ∈ s тогда и только тогда, когда b ∈ s.
LaTeX
$$$ a \in \operatorname{Stab}_G(s) \iff \forall b \in \alpha, \ a \cdot b \in s \iff b \in s $$$
Lean4
@[to_additive]
theorem mem_stabilizer_set {s : Set α} : a ∈ stabilizer G s ↔ ∀ b, a • b ∈ s ↔ b ∈ s :=
by
refine mem_stabilizer_iff.trans ⟨fun h b ↦ ?_, fun h ↦ ?_⟩
· rw [← (smul_mem_smul_set_iff : a • b ∈ _ ↔ _), h]
simp_rw [Set.ext_iff, mem_smul_set_iff_inv_smul_mem]
exact ((MulAction.toPerm a).forall_congr' <| by simp [Iff.comm]).1 h
