orbit_eq_range

Mathlib.Dynamics.Flow

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

English

The orbit of a point x under a flow is the set {ϕ(t)(x) : t ∈ τ}.

Русский

Орбитa точки x под потоком — это множество {ϕ(t)(x) : t ∈ τ}.

LaTeX

$$$\text{orbit}(x) = \{ \varphi(t)(x) : t \in \tau \}$$$

Lean4

theorem orbit_eq_range (x : α) : orbit ϕ x = Set.range (fun t => ϕ t x) :=
  rfl

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

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

Разделы

Аффилиация

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