of_finite

Mathlib.Analysis.Calculus.FDeriv.Basic

URI: https://scilib.ai/kg/mathlib#DifferentiableWithinAt.of_finite

English

If s is finite, then DifferentiableWithinAt 𝕜 f s x holds.

Русский

Если s конечное, то дифференцируемость внутри множества на точке x выполняется.

LaTeX

$$$$s\\text{ finite }\\Rightarrow \\text{DifferentiableWithinAt } 𝕜 f\\,s\\,x.$$$$

Lean4

theorem of_finite (h : s.Finite) : DifferentiableWithinAt 𝕜 f s x :=
  ⟨0, .of_finite h⟩

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

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

Разделы

Аффилиация

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