continuousWithinAt — Mathlib

English

If γ is an integral curve on s, then γ is continuous within s at any t0 ∈ s.

Русский

Если γ интегральная кривая на s, то она непрерывна внутри s в любой точке t0 ∈ s.

LaTeX

$$$\mathrm{IsMIntegralCurveOn}(\gamma,v,s) \Rightarrow \mathrm{ContinuousWithinAt}(\gamma,s,t_0).$$$

Lean4

theorem continuousWithinAt (hγ : IsMIntegralCurveOn γ v s) (ht : t₀ ∈ s) : ContinuousWithinAt γ s t₀ :=
  (hγ t₀ ht).1

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