sub — Mathlib

English

If p and q have MF-derivatives p' and q' on s, then their product p·q has a MF-derivative given by p z q' + p' q z with appropriate bilinear forms.

Русский

Если p и q имеют MF-деривативы на s, то произведение p·q имеет MF-дериватив, который выражается через p z q' + p' q z.

LaTeX

$$HasMFDerivWithinAt I 𝓘(𝕜,F') p s z p' → HasMFDerivWithinAt I 𝓘(𝕜,F') q s z q' → HasMFDerivWithinAt I 𝓘(𝕜,F') (p * q) s z (p z • q' + p' <• q z).$$

Lean4

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

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