contDiff

Mathlib.Analysis.SpecialFunctions.SmoothTransition

URI: https://scilib.ai/kg/mathlib#expNegInvGlue.contDiff

← MathLib Explorer

English

The function expNegInvGlue is smooth (infinitely differentiable).

Русский

Функция expNegInvGlue бесконечно гладкая.

LaTeX

$$$\text{ContDiff}{}_\mathbb{R}({\text{some order}})(\expNegInvGlue)$$$

Lean4

/-- The function `expNegInvGlue` is smooth. -/
@[fun_prop]
protected theorem contDiff {n : ℕ∞} : ContDiff ℝ n expNegInvGlue := by simpa using contDiff_polynomial_eval_inv_mul 1

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

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

Разделы

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

Аффилиация

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