ofQuotientStabilizer_mem_orbit

Mathlib.GroupTheory.GroupAction.Quotient

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

English

The image of a quotient stabilizer element lies in the orbit of x.

Русский

Изображение элемента факторного стабилизатора лежит в орбите x.

LaTeX

$$$\\operatorname{ofQuotientStabilizer}(\\alpha,x,g) \\in \\operatorname{orbit}(\\alpha,x)$$$

Lean4

@[to_additive]
theorem ofQuotientStabilizer_mem_orbit (g) : ofQuotientStabilizer α x g ∈ orbit α x :=
  Quotient.inductionOn' g fun g => ⟨g, rfl⟩

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

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

Разделы

Аффилиация

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