hasStrictFDerivAt_sub_const — Mathlib

English

The map t ↦ t − c has strict Fréchet derivative equal to the identity at any t ∈ F.

Русский

Функция t ↦ t − c имеет строгий Фреше-дифференциал в любой точке t, равный идентичности.

LaTeX

$$$ HasStrictFDerivAt (t \\mapsto t - c) \\mathrm{Id} \\; x $$$

Lean4

@[fun_prop]
theorem hasStrictFDerivAt_sub_const {x : F} (c : F) : HasStrictFDerivAt (· - c) (.id 𝕜 F) x :=
  (hasStrictFDerivAt_id x).sub_const c

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