mem_stabilizer_set_iff_smul_set_subset

English

Let G act on α and let s ⊆ α be finite. Then for every a ∈ G, a ∈ stabilizer G s if and only if a · s ⊆ s.

Русский

Пусть G действует на α и пусть s ⊆ α конечно. Тогда для любого a ∈ G верно: a ∈ стабилизатор G s тогда и только тогда, когда a · s ⊆ s.

LaTeX

$$$a \in \mathrm{Stab}_G(s) \;\Longleftrightarrow\; a \cdot s \subseteq s$$$

Lean4

@[to_additive]
theorem mem_stabilizer_set_iff_smul_set_subset {s : Set α} (hs : s.Finite) : a ∈ stabilizer G s ↔ a • s ⊆ s :=
  by
  lift s to Finset α using hs
  classical
    rw [stabilizer_coe_finset, mem_stabilizer_finset_iff_smul_finset_subset, ← Finset.coe_smul_finset,
    Finset.coe_subset]

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