hasFDerivAt_id — Mathlib

English

The identity map on E has Fréchet derivative at x equal to the identity linear map, i.e., its derivative exists and is the identity operator.

Русский

У тождественного отображения на E существует Фреше-производная в точке x, равная тождественному линейному отображению.

LaTeX

$$$\operatorname{HasFDerivAt}(\mathrm{id}_E, \mathrm{Id}_E, x)$$$

Lean4

@[fun_prop]
theorem hasFDerivAt_id (x : E) : HasFDerivAt id (.id 𝕜 E) x :=
  hasFDerivAtFilter_id _ _

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