stabilizer_finite — Mathlib

English

If s is nonempty and finite, then the stabilizer of s is finite.

Русский

Если s непусто и конечна, стабилизатор s конечно.

LaTeX

$$$ s \neq \varnothing \land s\text{ finite } \Rightarrow (\operatorname{Stab}_G(s)) \text{ finite }$$$

Lean4

@[to_additive]
theorem stabilizer_finite (hs₀ : s.Nonempty) (hs : s.Finite) : (stabilizer G s : Set G).Finite :=
  by
  obtain ⟨a, ha⟩ := hs₀
  exact (hs.div <| finite_singleton _).subset <| stabilizer_subset_div_right ha

Похожие утверждения