mem_stabilizer_finset' — Mathlib

English

The primed version of stabilizer membership equates to a subset condition on the smul by a.

Русский

Примечание к членству в стабилизаторе Finset′: эквивалентно условию подмножества после умножения на a.

LaTeX

$$$ a \in \operatorname{Stabilizer}_G(s) \iff \forall b \in s, a \cdot b \in s $$$

Lean4

@[to_additive]
theorem mem_stabilizer_finset' {s : Finset α} : a ∈ stabilizer G s ↔ ∀ ⦃b⦄, b ∈ s → a • b ∈ s :=
  by
  rw [← Subgroup.inv_mem_iff, mem_stabilizer_finset_iff_subset_smul_finset]
  simp_rw [← Finset.mem_inv_smul_finset_iff, Finset.subset_iff]

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