continuousAt — Mathlib

English

If f is MDifferentiableAt, then DifferentiableWithinAt writtenInExtChartAt holds on the chart domain.

Русский

Если f дифференцируема в модели, то дифференцируемость в записанной в extChart форме верна на области карты.

LaTeX

$$$\text{MDifferentiableAt } I I' f x \Rightarrow \text{DifferentiableWithinAt } 𝕜 (writtenInExtChartAt I I' x f) (\text{range } I) ((\text{extChartAt } I x) x)$$$

Lean4

theorem continuousAt {f : M → M'} {x : M} (hf : MDifferentiableAt I I' f x) : ContinuousAt f x :=
  mdifferentiableAt_iff .. |>.1 hf |>.1

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