mul' — Mathlib

English

Negation preserves MF-derivative: if f has MF-derivative f' at z, then −f has MF-derivative −f' at z.

Русский

Отрицание сохраняет MF-дериватив: если f имеет MF-дериватив f' в z, то −f имеет MF-дериватив −f' в z.

LaTeX

$$HasMFDerivAt I 𝓘(𝕜,E') f z f' → HasMFDerivAt I 𝓘(𝕜,E') (−f) z (−f')$$

Lean4

theorem mul' (hp : HasMFDerivAt I 𝓘(𝕜, F') p z p') (hq : HasMFDerivAt I 𝓘(𝕜, F') q z q') :
    HasMFDerivAt I 𝓘(𝕜, F') (p * q) z (p z • q' + p' <• q z : E →L[𝕜] F') :=
  hasMFDerivWithinAt_univ.mp <| hp.hasMFDerivWithinAt.mul' hq.hasMFDerivWithinAt

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