star

Mathlib.Analysis.Calculus.Deriv.Star

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

English

If HasDerivAt g g' x, then HasDerivAt (star ∘ g) (star g') x.

Русский

Если есть HasDerivAt g g' x, то HasDerivAt star(g) star(g') x.

LaTeX

$$HasDerivAt g g' x → HasDerivAt (fun x => star (g x)) (star g') x$$

Lean4

protected nonrec theorem star (h : HasDerivAt f f' x) : HasDerivAt (fun x => star (f x)) (star f') x :=
  h.star

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

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

Разделы

Аффилиация

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