orbit_smul_subset

Mathlib.GroupTheory.GroupAction.Defs

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

← MathLib Explorer

English

If S is a submonoid of M, then the S-orbit of a is contained in the M-orbit of a.

Русский

Если S — подмоноид M, то S-орбита a ⊆ M-орбиты a.

LaTeX

$$$\operatorname{orbit}(S,a) \subseteq \operatorname{orbit}(M,a)$$$

Lean4

@[to_additive]
theorem orbit_smul_subset (m : M) (a : α) : orbit M (m • a) ⊆ orbit M a :=
  Set.range_subset_iff.2 fun m' => mul_smul m' m a ▸ mem_orbit _ _

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

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

Разделы

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

Аффилиация

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