orbit

Mathlib.GroupTheory.GroupAction.Blocks

URI: https://scilib.ai/kg/mathlib#MulAction.IsBlock.orbit

← MathLib Explorer

English

Let G act on X. Then the orbit of any point a ∈ X is a block under the G-action.

Русский

Пусть G действует на X. Орбита элемента a ∈ X является блоком относительно действия G.

LaTeX

$$$IsBlock\;G\;(orbit\,G\ a)$$$

Lean4

/-- An orbit is a block. -/
@[to_additive /-- An orbit is a block. -/
    ]
protected theorem orbit (a : X) : IsBlock G (orbit G a) :=
  (IsFixedBlock.orbit a).isBlock

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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