denseRange_smul

Mathlib.Dynamics.Minimal

URI: https://scilib.ai/kg/mathlib#denseRange_smul

English

Under a minimal action, the map c ↦ c•x has dense range in α.

Русский

При минимальном действии отображение c ↦ c•x имеет плотный образ в α.

LaTeX

$$$\\text{DenseRange}(c \\mapsto c \\cdot x)$.$$

Lean4

@[to_additive]
theorem denseRange_smul [IsMinimal M α] (x : α) : DenseRange fun c : M ↦ c • x :=
  MulAction.dense_orbit M x

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

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

Разделы

Аффилиация

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