smul

Mathlib.Analysis.Calculus.FDeriv.Mul

URI: https://scilib.ai/kg/mathlib#HasFDerivWithinAt.smul

← MathLib Explorer

English

Same product rule as HasStrictFDerivAt but within a set s.

Русский

То же правило произведения, но внутри множества s.

LaTeX

$$$$ \\text{HasFDerivWithinAt}(\\lambda y, c(y)·f(y), s, x) = c(x)·f' + c'.smulRight(f(x)). $$$$

Lean4

@[fun_prop]
theorem smul (hc : HasFDerivWithinAt c c' s x) (hf : HasFDerivWithinAt f f' s x) :
    HasFDerivWithinAt (c • f) (c x • f' + c'.smulRight (f x)) s x :=
  hc.fun_smul hf

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru