fst — Mathlib

English

The derivative of the fst projection for a product map is the composition of fst with the derivative of the inner map.

Русский

Производная проекции fst для отображения произведения равна композиции fst с производной внутреннего отображения.

LaTeX

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

Lean4

@[fun_prop]
protected nonrec theorem fst (h : HasFDerivWithinAt f₂ f₂' s x) :
    HasFDerivWithinAt (fun x => (f₂ x).1) ((fst 𝕜 F G).comp f₂') s x :=
  h.fst

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