snd — Mathlib

English

If f₂ has strict derivative f₂' at x, then the derivative of the second component is the composition of the second projection with f₂'.

Русский

Если f₂ имеет строгую производную f₂' в точке x, производная второй компоненты равна композиции проекции snd с f₂'.

LaTeX

$$$\text{HasStrictFDerivAt} f₂ f₂' x \quad\Rightarrow\quad \text{HasStrictFDerivAt} (\lambda x, (f₂ x)_2) ((\text{snd } 𝕜 F G) \circ f₂') x$$$

Lean4

@[fun_prop]
protected theorem snd (h : HasStrictFDerivAt f₂ f₂' x) :
    HasStrictFDerivAt (fun x => (f₂ x).2) ((snd 𝕜 F G).comp f₂') x :=
  hasStrictFDerivAt_snd.comp x h

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