add — Mathlib

English

The tangent map of the product map in the right component is the pairing of the right projection with the derivative component.

Русский

Касательная карта произведения по правой компоненте — это пара правой проекции и касательной по правой компоненте.

LaTeX

$$$tangentMap\ (I'\ prod I) I' (Prod.snd) p = ⟨p.proj.2, p.2.2⟩$$$

Lean4

theorem add (hf : MDifferentiableAt I 𝓘(𝕜, E') f z) (hg : MDifferentiableAt I 𝓘(𝕜, E') g z) :
    MDifferentiableAt I 𝓘(𝕜, E') (f + g) z :=
  (hf.hasMFDerivAt.add hg.hasMFDerivAt).mdifferentiableAt

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