mem_stabilizer_finset_iff_smul_finset_subset

English

Membership is equivalent to the smul of the Finset by a being contained in the Finset.

Русский

Принадлежность эквивалентна тому, что a • s ⊆ s.

LaTeX

$$$ a \in Stabilizer G s \iff a \cdot s \subseteq s $$$

Lean4

@[to_additive]
theorem mem_stabilizer_finset_iff_smul_finset_subset {s : Finset α} : a ∈ stabilizer G s ↔ a • s ⊆ s := by
  rw [mem_stabilizer_iff, Finset.subset_iff_eq_of_card_le (Finset.card_smul_finset _ _).ge]

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