differentiableAt_fst

Mathlib.Analysis.Calculus.FDeriv.Prod

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

English

The projection to the first coordinate, Prod.fst: E × F → E, is differentiable at every point.

Русский

Проекция на первую координату, Prod.fst: E × F → E, дифференцируема в любой точке.

LaTeX

$$$\text{DifferentiableAt } 𝕜\bigl(\text{Prod.fst}\bigr)\ p$$$

Lean4

@[fun_prop]
theorem differentiableAt_fst : DifferentiableAt 𝕜 Prod.fst p :=
  hasFDerivAt_fst.differentiableAt

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

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

Разделы

Аффилиация

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