differentiableWithinAt_fst — Mathlib

English

The derivative of the first projection is the simple projection map: fderiv 𝕜 Prod.fst p equals fst 𝕜 E F.

Русский

Производная от проекции на первую координату равна самой проекции: fderiv 𝕜 Prod.fst p = fst 𝕜 E F.

LaTeX

$$$\text{fderiv } 𝕜\big(\text{Prod.fst}\big) p = \text{fst } 𝕜 E F$$$

Lean4

@[fun_prop]
theorem differentiableWithinAt_fst {s : Set (E × F)} : DifferentiableWithinAt 𝕜 Prod.fst s p :=
  differentiableAt_fst.differentiableWithinAt

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