snd — Mathlib

English

The second projection has a derivative at p equal to the second projection map.

Русский

У второй проекции Pro d имеет производную в p, равную самой проекции snd.

LaTeX

$$HasFDerivAt Prod.snd (ContinuousLinearMap.snd 𝕜 E F) p$$

Lean4

protected theorem snd (h : HasFDerivAtFilter f₂ f₂' x L) :
    HasFDerivAtFilter (fun x => (f₂ x).2) ((snd 𝕜 F G).comp f₂') x L :=
  hasFDerivAtFilter_snd.comp x h tendsto_map

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