unique

Mathlib.Analysis.Calculus.Deriv.Basic

URI: https://scilib.ai/kg/mathlib#HasDerivAt.unique

English

If HasDerivAt f f0' x and HasDerivAt f f1' x hold, then f0' = f1'.

Русский

Если существуют две производные в одной точке, они совпадают.

LaTeX

$$$\text{HasDerivAt } f\; f_0'\; x \Rightarrow \text{HasDerivAt } f\; f_1'\; x \Rightarrow f_0' = f_1'$$$

Lean4

theorem unique (h₀ : HasDerivAt f f₀' x) (h₁ : HasDerivAt f f₁' x) : f₀' = f₁' :=
  smulRight_one_eq_iff.mp <| h₀.hasFDerivAt.unique h₁

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

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

Разделы

Аффилиация

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