mul_const — Mathlib

English

If hc is HasDerivWithinAt for c with derivative c' and d is a constant, then HasDerivWithinAt for y ↦ c(y) · d has derivative c' · d.

Русский

Если hc задаёт производную внутри для c и d константа, то производная внутри для y ↦ c(y) · d равна c'(x) · d.

LaTeX

$$$\text{HasDerivWithinAt}(y \mapsto c(y) \cdot d) (s) x = c'(x) \cdot d$$$

Lean4

theorem mul_const (hc : HasDerivAt c c' x) (d : 𝔸) : HasDerivAt (fun y => c y * d) (c' * d) x :=
  by
  rw [← hasDerivWithinAt_univ] at *
  exact hc.mul_const d

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