mem_orbit_self

Mathlib.GroupTheory.GroupAction.Defs

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

English

Any element a of α lies in its own orbit under the action, via the identity element acting once.

Русский

Любой элемент a множества α принадлежит своей орбите под действием тождественного элемента.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem mem_orbit_self (a : α) : a ∈ orbit M a :=
  ⟨1, by simp⟩

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

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

Разделы

Аффилиация

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