hasFDerivWithinAt_snd

Mathlib.Analysis.Calculus.FDeriv.Prod

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

English

The snd projection is differentiable at every point.

Русский

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

LaTeX

$$differentiable_snd : Differentiable 𝕜 Prod.snd p$$

Lean4

@[fun_prop]
theorem hasFDerivWithinAt_snd {s : Set (E × F)} : HasFDerivWithinAt (@Prod.snd E F) (snd 𝕜 E F) s p :=
  hasFDerivAtFilter_snd

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

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

Разделы

Аффилиация

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