English
A subgroup H of G is contained in the stabilizer of a set s if and only if for every g in H, g•s ⊆ s.
Русский
Подгруппа H группы G входит в стабилизатор множества s тогда и только тогда, когда для каждого g ∈ H выполняется g•s ⊆ s.
LaTeX
$$$H \\leq \\mathrm{stabilizer}_G(s) \\;\\iff\\; \\forall g \\in H, \\; g \\cdot s \\subseteq s$$$
Lean4
/-- To prove inclusion of a *subgroup* in a stabilizer, it is enough to prove inclusions. -/
@[to_additive /-- To prove inclusion of a *subgroup* in a stabilizer, it is enough to prove inclusions. -/
]
theorem le_stabilizer_iff_smul_le (s : Set α) (H : Subgroup G) : H ≤ stabilizer G s ↔ ∀ g ∈ H, g • s ⊆ s :=
by
constructor
· intro hyp g hg
apply Eq.subset
rw [← mem_stabilizer_iff]
exact hyp hg
· intro hyp g hg
rw [mem_stabilizer_iff]
apply subset_antisymm (hyp g hg)
intro x hx
use g⁻¹ • x
constructor
· apply hyp g⁻¹ (inv_mem hg)
simp only [Set.smul_mem_smul_set_iff, hx]
· simp only [smul_inv_smul]
