differentiableAt_one

Mathlib.Analysis.Calculus.FDeriv.Const

URI: https://scilib.ai/kg/mathlib#differentiableAt_one

English

The constant map f(y) = 1 is differentiable at every x.

Русский

Пусть f(y) = 1. Этот отображение дифференцируемо в любой точке x.

LaTeX

$$DifferentiableAt 𝕜 (1 : E → F) x$$

Lean4

@[simp, fun_prop]
theorem differentiableAt_one [One F] (x : E) : DifferentiableAt 𝕜 (1 : E → F) x :=
  differentiableAt_const _

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

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

Разделы

Аффилиация

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