mem_stabilizer_finset_iff_subset_smul_finset

English

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

Русский

Принадлежность стабилизатору Finset эквивалентна подмножеству Finset внутри a • Finset.

LaTeX

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

Lean4

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

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