mem_orbit_of_mem_forwardOrbit

Mathlib.Dynamics.Flow

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

English

If a point x1 lies in the forward orbit of x2, then x1 lies in the orbit of x2.

Русский

Если точка x1 принадлежит прямой орбите x2, то она принадлежит орбите x2.

LaTeX

$$$x_1 \\in forwardOrbit\\\\ ϕ x_2 \\Rightarrow x_1 \\in orbit\\\\ ϕ x_2.$$$

Lean4

theorem mem_orbit_of_mem_forwardOrbit {x₁ x₂ : α} (h : x₁ ∈ forwardOrbit ϕ x₂) : x₁ ∈ orbit ϕ x₂ :=
  ϕ.forwardOrbit_subset_orbit x₂ h

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

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

Разделы

Аффилиация

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