mem_orbit_of_mem_orbit_submonoid

Mathlib.GroupTheory.GroupAction.Defs

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

← MathLib Explorer

English

If a is in the orbit of b under a submonoid S, then a is in the M-orbit of b for the ambient M.

Русский

Если a лежит в орбите b по S, то a лежит и в орбите b по M.

LaTeX

$$$ a \in \operatorname{orbit}(S,b) \Rightarrow a \in \operatorname{orbit}(M,b) $$$

Lean4

@[to_additive]
theorem mem_orbit_of_mem_orbit_submonoid {S : Submonoid M} {a b : α} (h : a ∈ orbit S b) : a ∈ orbit M b :=
  orbit_submonoid_subset S _ h

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

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

Разделы

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

Аффилиация

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