mem_stabilizer_finset — Mathlib

English

A stability equivalence for Finset: membership in stabilizer is characterized by a condition on all elements.

Русский

Эквивалентность принадлежности стабилизатору Finset через условие на все элементы.

LaTeX

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

Lean4

@[to_additive]
theorem mem_stabilizer_finset {s : Finset α} : a ∈ stabilizer G s ↔ ∀ b, a • b ∈ s ↔ b ∈ s := by
  simp_rw [← stabilizer_coe_finset, mem_stabilizer_set, Finset.mem_coe]

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