differentiable_one

Mathlib.Analysis.Calculus.ContDiff.Defs

URI: https://scilib.ai/kg/mathlib#ContDiff.differentiable_one

← MathLib Explorer

English

From C^(n+1) to C^n, decreasing the order by one preserves ContDiff.

Русский

Из C^(n+1) следует C^n, понижая порядок на единицу, сохраняется ContDiff.

LaTeX

$$$ContDiff\ 𝕜\ (n+1) f \Rightarrow ContDiff 𝕜\ n f$$$

Lean4

@[fun_prop]
theorem differentiable_one (h : ContDiff 𝕜 1 f) : Differentiable 𝕜 f :=
  differentiableOn_univ.1 <| (contDiffOn_univ.2 h).differentiableOn (le_refl 1)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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