isForwardInvariant_forwardOrbit — Mathlib

English

The forward orbit is forward-invariant under ϕ; equivalently, for every t, ϕ(t) maps forwardOrbit ϕ x into itself.

Русский

Прямая орбита инвариантна по времени относительно потока ϕ; то есть для каждого t отображение ϕ(t) переводит forwardOrbit ϕ x в саму forwardOrbit ϕ x.

LaTeX

$$$IsForwardInvariant(\\\\varphi)(forwardOrbit\\\\ ϕ x).$$$

Lean4

/-- The forward orbit of a point under a flow `ϕ` is forward-invariant under `ϕ`. -/
theorem isForwardInvariant_forwardOrbit (x : α) : IsForwardInvariant ϕ (forwardOrbit ϕ x) := fun t h =>
  IsInvariant.isForwardInvariant (isInvariant_orbit ϕ.restrictNonneg x) (t := ⟨t, h⟩) h

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