prodMap — Mathlib

English

General version of HasStrictFDerivAt.prodMap for maps f and f₂ with derivatives f' and f₂'.

Русский

Общая версия HasStrictFDerivAt.prodMap для функций f и f₂ с производными 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 : HasFDerivAt f f' p.1) (hf₂ : HasFDerivAt f₂ f₂' p.2) :
    HasFDerivAt (Prod.map f f₂) (f'.prodMap f₂') p :=
  (hf.comp p hasFDerivAt_fst).prodMk (hf₂.comp p hasFDerivAt_snd)

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