dense_orbit

Mathlib.Dynamics.Minimal

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

English

For a minimal action of a monoid M on α, the orbit of any x is dense in α.

Русский

При минимальном действии моноида M на α орбита любой точки плотна в α.

LaTeX

$$$Dense(orbit\\, M\\, x) \\\\text{ (equivalently } \\overline{orbit\\, M\\, x} = \\alpha).$$$

Lean4

@[to_additive]
theorem dense_orbit [IsMinimal M α] (x : α) : Dense (orbit M x) :=
  MulAction.IsMinimal.dense_orbit x

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

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

Разделы

Аффилиация

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