derivWithin_const_mul_field — Mathlib

English

If u is a constant and v is a function, then the derivative within s of y ↦ u · v(y) is u times the derivative within s of v.

Русский

Если u — константа, а v — функция, то внутри s производная от y ↦ u · v(y) равна u · производной внутри s от v.

LaTeX

$$$ \mathrm{derivWithin}_s (u \cdot v)(x) = u \cdot \mathrm{derivWithin}_s v(x) $$$

Lean4

theorem derivWithin_const_mul_field (u : 𝕜') : derivWithin (fun y => u * v y) s x = u * derivWithin v s x :=
  by
  simp_rw [mul_comm u]
  exact derivWithin_mul_const_field u

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