fderiv_id'

Mathlib.Analysis.Calculus.FDeriv.Basic

URI: https://scilib.ai/kg/mathlib#fderiv_id'

English

The derivative of the fun x ↦ x at x is the identity map; equivalently fderiv 𝕜 (fun x => x) x = id 𝕜 E.

Русский

Производная от fun x => x в точке x равна идентичному отображению.

LaTeX

$$$\mathrm{fderiv}_{\mathbb{K}}(\mathrm{fun}\;x:\,E\to E\;\mapsto x, x) = \mathrm{Id}_{\mathbb{K}} E$$$

Lean4

@[simp]
theorem fderiv_id' : fderiv 𝕜 (fun x : E => x) x = ContinuousLinearMap.id 𝕜 E :=
  fderiv_id

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

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

Разделы

Аффилиация

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