snd — Mathlib

English

If f is strictly differentiable at p and f₂ is strictly differentiable at p, then Prod.map f f₂ is strictly differentiable with derivative f' ∘ f₂'.

Русский

Если f и f₂ строго дифференцируемы в p, то Prod.map f f₂ строго дифференцируем и его производная равна f'∘f₂'.

LaTeX

$$HasStrictFDerivAt.prodMap (hf) (hf₂) : HasStrictFDerivAt (Prod.map f f₂) (f'.prodMap f₂') p$$

Lean4

@[simp, fun_prop]
protected theorem snd (h : Differentiable 𝕜 f₂) : Differentiable 𝕜 fun x => (f₂ x).2 :=
  differentiable_snd.comp h

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