continuousOn

Mathlib.Analysis.Calculus.FDeriv.Basic

URI: https://scilib.ai/kg/mathlib#DifferentiableOn.continuousOn

English

Differentiability on a set implies continuity on that set.

Русский

Дифференцируемость на множестве подразумевает непрерывность на этом множестве.

LaTeX

$$DifferentiableOn 𝕜 f s → ContinuousOn f s$$

Lean4

@[fun_prop]
theorem continuousOn (h : DifferentiableOn 𝕜 f s) : ContinuousOn f s := fun x hx => (h x hx).continuousWithinAt

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

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

Разделы

Аффилиация

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