scomp_of_eq

Mathlib.Analysis.Calculus.Deriv.Comp

URI: https://scilib.ai/kg/mathlib#HasDerivWithinAt.scomp_of_eq

Lean4

theorem scomp_of_eq (hg : HasDerivWithinAt g₁ g₁' t' y) (hh : HasDerivWithinAt h h' s x) (hst : MapsTo h s t')
    (hy : y = h x) : HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x := by rw [hy] at hg; exact hg.scomp x hh hst

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

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

Разделы

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

Аффилиация

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