stabilizer_le_aestabilizer

Mathlib.MeasureTheory.Group.AEStabilizer

URI: https://scilib.ai/kg/mathlib#MulAction.stabilizer_le_aestabilizer

English

The set-theoretic stabilizer of s is contained in the a.e.-stabilizer of s.

Русский

Стандартный стабилизатор множества s содержится в ae-стабилизаторе s.

LaTeX

$$$stabilizer(G,s) \leq aestabilizer(G,\mu,s)$$$

Lean4

@[to_additive]
theorem stabilizer_le_aestabilizer (s : Set α) : stabilizer G s ≤ aestabilizer G μ s :=
  by
  intro g hg
  simp_all

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru