fderiv_snd

Mathlib.Analysis.Calculus.FDeriv.Prod

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

English

The snd projection is differentiable at every point.

Русский

Проекция snd дифференцируема в любой точке.

LaTeX

$$differentiable_snd : Differentiable 𝕜 Prod.snd$$

Lean4

theorem fderiv_snd : fderiv 𝕜 Prod.snd p = snd 𝕜 E F :=
  hasFDerivAt_snd.fderiv

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

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

Разделы

Аффилиация

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