mem_stabilizer_set_iff_subset_smul_set

English

For a finite set s, a belongs to stabilizer of s iff s ⊆ a • s.

Русский

Для конечного множества s: a принадлежит стабилизатору s тогда и только тогда, когда s ⊆ a • s.

LaTeX

$$$ a \in stabilizer_G(s) \quad \text{ (hs: s.Finite) } \iff s \subseteq a \cdot s $$$

Lean4

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

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