prodMap — Mathlib

English

The map Prod.map f f₂ is strictly differentiable at p when f and f₂ are strictly differentiable at their respective points.

Русский

Производна Prod.map f f₂ существует и является строгой при p, если f и f₂ строго дифференцируемы в своих точках.

LaTeX

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

Lean4

@[fun_prop]
protected theorem prodMap (hf : HasStrictFDerivAt f f' p.1) (hf₂ : HasStrictFDerivAt f₂ f₂' p.2) :
    HasStrictFDerivAt (Prod.map f f₂) (f'.prodMap f₂') p :=
  (hf.comp p hasStrictFDerivAt_fst).prodMk (hf₂.comp p hasStrictFDerivAt_snd)

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