mem_orbit_self

Mathlib.Dynamics.Flow

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

English

x belongs to its own orbit: x ∈ orbit ϕ x.

Русский

x принадлежит своей орбите: x ∈ orbit ϕ x.

LaTeX

$$$x \in \mathrm{orbit}(\varphi, x)$$$

Lean4

theorem mem_orbit_self (x : α) : x ∈ orbit ϕ x :=
  ϕ.toAddAction.mem_orbit_self x

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

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

Разделы

Аффилиация

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