hasStrictFDerivAt_fst — Mathlib

English

The first projection map Prod.fst is strictly Frechet differentiable with derivative fst 𝕜 E F at any point p.

Русский

Первая проекция Prod.fst строго Фредже-дифференцируема; производная равна fst 𝕜 E F.

LaTeX

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

Lean4

@[fun_prop]
theorem hasStrictFDerivAt_fst : HasStrictFDerivAt (@Prod.fst E F) (fst 𝕜 E F) p :=
  (fst 𝕜 E F).hasStrictFDerivAt

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