orbit

Mathlib.Dynamics.Flow

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

English

If t is continuous and f is continuous, then the map x ↦ ϕ (t x) (f x) is continuous.

Русский

Если t непрерывна и f непрерывна, то отображение x ↦ ϕ(t(x))(f(x)) непрерывно.

LaTeX

$$$\text{Continuous } t \Rightarrow \text{Continuous } f \Rightarrow \text{Continuous }(x \mapsto \varphi(t(x))(f(x))).$$$

Lean4

/-- The orbit of a point under a flow. -/
def orbit (x : α) : Set α :=
  ϕ.toAddAction.orbit _ x

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

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

Разделы

Аффилиация

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