continuousAt

Mathlib.Analysis.Calculus.FDeriv.Basic

URI: https://scilib.ai/kg/mathlib#HasStrictFDerivAt.continuousAt

English

A strong Frechet derivative implies continuity of f.

Русский

Сильная производная Фреше влечет непрерывность f.

LaTeX

$$HasStrictFDerivAt f f' x → ContinuousAt f x$$

Lean4

protected theorem continuousAt (hf : HasStrictFDerivAt f f' x) : ContinuousAt f x :=
  hf.hasFDerivAt.continuousAt

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

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

Разделы

Аффилиация

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