mul' — Mathlib

English

If p and q are MF-differentiable at z with derivatives p', q', then the product p·q has MF-derivative given by a bilinear combination of p, p', q, q'.

Русский

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

LaTeX

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

Lean4

theorem mul' (hp : HasMFDerivWithinAt I 𝓘(𝕜, F') p s z p') (hq : HasMFDerivWithinAt I 𝓘(𝕜, F') q s z q') :
    HasMFDerivWithinAt I 𝓘(𝕜, F') (p * q) s z (p z • q' + p' <• q z : E →L[𝕜] F') :=
  ⟨hp.1.mul hq.1, by simpa only [mfld_simps] using hp.2.mul' hq.2⟩

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