forwardOrbit_eq_range_nonneg

Mathlib.Dynamics.Flow

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

English

The forward orbit of x is the range of the map t ↦ ϕ t x over nonnegative t.

Русский

Прямая орбита x есть множество всех значений ϕ t x при t ≥ 0.

LaTeX

$$$forwardOrbit\\\\ ϕ x = \\operatorname{Set.range}(\\\\lambda t : {t : \\tau \\mid 0 \\le t},\\\\ \\\\varphi t x).$$$

Lean4

theorem forwardOrbit_eq_range_nonneg (x : α) : forwardOrbit ϕ x = Set.range (fun t : { t : τ // 0 ≤ t } => ϕ t x) :=
  rfl

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

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

Разделы

Аффилиация

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