hasFDerivAtFilter_snd

Mathlib.Analysis.Calculus.FDeriv.Prod

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

English

For any filter L, the derivative at p of the second projection is the second projection composed with f₂'.

Русский

Для любого фильтра L производная по snd в p равна snd ∘ f₂'.

LaTeX

$$HasFDerivAtFilter Prod.snd (ContinuousLinearMap.snd 𝕜 E F) p L$$

Lean4

theorem hasFDerivAtFilter_snd {L : Filter (E × F)} : HasFDerivAtFilter (@Prod.snd E F) (snd 𝕜 E F) p L :=
  (snd 𝕜 E F).hasFDerivAtFilter

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

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

Разделы

Аффилиация

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