forwardOrbit — Mathlib

English

The forward orbit of a point x is the orbit of x under the restricted flow ϕ.restrictNonneg; it consists of all states reached by nonnegative time along the flow.

Русский

Прямая орбита точки x — орбита x под ограниченным потоком ϕ, состоящая из состояний, достигаемых за неотрицательное время вдоль потока.

LaTeX

$$$forwardOrbit(\\\\varphi)(x) = orbit(\\\\varphi.nonneg)\\, x.$$$

Lean4

/-- The forward orbit of a point under a flow. -/
def forwardOrbit (x : α) : Set α :=
  orbit ϕ.restrictNonneg x

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