continuousAt — Mathlib

English

If γ is integral at t0, then γ is continuous at t0.

Русский

Если γ интегральна в точке t0, то она непрерывна в t0.

LaTeX

$$$\mathrm{IsMIntegralCurveAt}(\gamma,v,t_0) \Rightarrow \mathrm{ContinuousAt}(\gamma,t_0).$$$

Lean4

theorem continuousAt (hγ : IsMIntegralCurveAt γ v t₀) : ContinuousAt γ t₀ :=
  have ⟨_, hs, hγ⟩ := isMIntegralCurveAt_iff.mp hγ
  hγ.continuousWithinAt (mem_of_mem_nhds hs) |>.continuousAt hs

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