continuousWithinAt

Mathlib.Analysis.Calculus.Deriv.Basic

URI: https://scilib.ai/kg/mathlib#HasDerivWithinAt.continuousWithinAt

English

If HasDerivWithinAt f f' s x holds for every x in s, then f is ContinuousOn s.

Русский

Если для каждого x ∈ s верно HasDerivWithinAt f f'(x) x, то f непрерывна на s.

LaTeX

$$$\\forall x \\in s,\\ HasDerivWithinAt\\ f\\ (f'(x))\\ s\\ x\\Rightarrow\\ ContinuousOn\\ f\\ s$$$

Lean4

theorem continuousWithinAt (h : HasDerivWithinAt f f' s x) : ContinuousWithinAt f s x :=
  HasDerivAtFilter.tendsto_nhds inf_le_left h

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

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

Разделы

Аффилиация

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