hasFDerivAtFilter_fst

Mathlib.Analysis.Calculus.FDeriv.Prod

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

English

The first projection Prod.fst has a Frechet derivative given by fst 𝕜 E F at p.

Русский

Первая проекция Prod.fst имеет Фредже-производную fst 𝕜 E F в точке p.

LaTeX

$$$\text{HasFDerivAt}\big(\mathrm{Prod.fst}, \mathrm{fst}\, 𝕜\, E\, F\big)\; p$$$

Lean4

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

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

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

Разделы

Аффилиация

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