dslope_same

Mathlib.Analysis.Calculus.DSlope

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

English

Reiterates that dslope at equal arguments matches deriv.

Русский

Повторение того, что dslope на равных аргументах совпадает с производной.

LaTeX

$$$ dslope\ f\ a\ a = deriv\ f\ a $$$

Lean4

@[simp]
theorem dslope_same (f : 𝕜 → E) (a : 𝕜) : dslope f a a = deriv f a := by classical exact update_self ..

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

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

Разделы

Аффилиация

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