stabilizer_singleton — Mathlib

English

The stabilizer of a singleton {b} equals the stabilizer of the element b: stabilizer_G({b}) = stabilizer_G(b).

Русский

Стабилизатор множества {b} равен стабилизатору элемента b: stabilizer_G({b}) = stabilizer_G(b).

LaTeX

$$$\operatorname{stabilizer}_G(\{b\}) = \operatorname{stabilizer}_G(b)$$$

Lean4

@[to_additive (attr := simp)]
theorem stabilizer_singleton (b : α) : stabilizer G ({ b } : Set α) = stabilizer G b := by ext; simp

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