add — Mathlib

English

The derivative with respect to a map into a product equals the sum of the derivatives with respect to each coordinate, as a function of a pair; expressed via the coprod structure.

Русский

Производная отображения в произведение равна сумме производных по каждой координате, как функция двойки.

LaTeX

$$$mfderiv\ (I.prod I') I'' f p = (mfderiv I I'' (fun z => f (z, p.2)) p.1) ∘L (fst) + (mfderiv I' I'' (fun z => f (p.1, z)) p.2) ∘L (snd)$$$

Lean4

theorem add (hf : HasMFDerivAt I 𝓘(𝕜, E') f z f') (hg : HasMFDerivAt I 𝓘(𝕜, E') g z g') :
    HasMFDerivAt I 𝓘(𝕜, E') (f + g) z (f' + g') :=
  ⟨hf.1.add hg.1, hf.2.add hg.2⟩

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