mul — Mathlib

English

If f and g are MDifferentiable on M, then their product f·g is MDifferentiable on M.

Русский

Если f и g дифференцируемы на M, то их произведение f·g дифференцируемо на M.

LaTeX

$$MDifferentiable I 𝓘(𝕜,E') f → MDifferentiable I 𝓘(𝕜,E') g → MDifferentiable I 𝓘(𝕜,E') (f·g)$$

Lean4

theorem mul (hp : MDifferentiable I 𝓘(𝕜, F') p) (hq : MDifferentiable I 𝓘(𝕜, F') q) :
    MDifferentiable I 𝓘(𝕜, F') (p * q) := fun x => (hp x).mul (hq x)

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