fderiv_fst — Mathlib

English

The derivative of the first projection is the standard projection; the formula expresses this in terms of linear maps.

Русский

Производная от проекции на первую координату — стандартная проекция; формула выражает это через линейные отображения.

LaTeX

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

Lean4

theorem fderiv_fst : fderiv 𝕜 Prod.fst p = fst 𝕜 E F :=
  hasFDerivAt_fst.fderiv

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