dslope_sub_smul_of_ne

Mathlib.Analysis.Calculus.DSlope

URI: https://scilib.ai/kg/mathlib#dslope_sub_smul_of_ne

← MathLib Explorer

English

If b ≠ a, then the slope of the function x ↦ (x − a) f(x) at the pair (a,b) equals f(b).

Русский

Если b ≠ a, то dslope( x ↦ (x − a) f(x) ) a b = f(b).

LaTeX

$$$dslope\bigl( x \mapsto (x - a) \cdot f(x) \bigr)\ a\ b = f(b)$$$

Lean4

theorem dslope_sub_smul_of_ne (f : 𝕜 → E) (h : b ≠ a) : dslope (fun x => (x - a) • f x) a b = f b := by
  rw [dslope_of_ne _ h, slope_sub_smul _ h.symm]

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

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

Разделы

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

Аффилиация

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