mem_orbit_of_mem_orbit — Mathlib

English

Let ϕ be a flow on α with time τ. If x2 lies in the orbit of x1 under ϕ, then for every t ∈ τ, ϕ(t) x2 also lies in the orbit of x1.

Русский

Пусть ϕ — поток на α с временем τ. Если x2 принадлежит орбите x1 под действием ϕ, то для любого t ∈ τ отображение ϕ(t) x2 также принадлежит той же орбите ϕ x1.

LaTeX

$$$\\\\forall x_1,x_2 \\in \\alpha \\\\,\\forall t \\in \\tau,\\ x_2 \\in \\operatorname{orbit}(\\\\varphi, x_1) \\Rightarrow \\\\varphi(t) x_2 \\in \\operatorname{orbit}(\\\\varphi, x_1).$$$

Lean4

theorem mem_orbit_of_mem_orbit {x₁ x₂ : α} (t : τ) (h : x₂ ∈ orbit ϕ x₁) : ϕ t x₂ ∈ orbit ϕ x₁ :=
  ϕ.toAddAction.mem_orbit_of_mem_orbit t h

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