continuous

Mathlib.Geometry.Manifold.IntegralCurve.Basic

URI: https://scilib.ai/kg/mathlib#IsMIntegralCurve.continuous

English

If γ is an integral curve, then γ is a continuous function.

Русский

Если γ интегральная кривая, тогда γ непрерывна как функция.

LaTeX

$$$\mathrm{IsMIntegralCurve}(\gamma,v) \Rightarrow \mathrm{Continuous}(\gamma).$$$

Lean4

theorem continuous (hγ : IsMIntegralCurve γ v) : Continuous γ :=
  continuous_iff_continuousAt.mpr fun t ↦ (hγ.isMIntegralCurveAt t).continuousAt

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

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

Разделы

Аффилиация

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