differentiableAt_fun_id — Mathlib

English

Variant stating that the identity map, viewed as a function, is differentiable; in particular, the derivative is the identity map.

Русский

Вариант утверждения: тождественное отображение дифференцируемо; производная равна тождественному линейному отображению.

LaTeX

$$$\mathrm{Differentiable}_{\mathbb{K}}(\mathrm{id}, x)$$$

Lean4

/-- Variant with `fun x => x` rather than `id` -/
@[simp, fun_prop]
theorem differentiableAt_fun_id : DifferentiableAt 𝕜 (fun x => x) x :=
  (hasFDerivAt_id x).differentiableAt

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