fst — Mathlib

English

The function Prod.fst: E × F → E is differentiable at every point; its derivative is the projection to the first coordinate.

Русский

Функция Prod.fst: E × F → E дифференцируема в каждой точке; её производная — проекция на первую координату.

LaTeX

$$$\text{DifferentiableAt } 𝕜\bigl(\text{Prod.fst}\bigr) = \text{the projection onto the first factor}$$$

Lean4

@[simp, fun_prop]
protected theorem fst (h : DifferentiableAt 𝕜 f₂ x) : DifferentiableAt 𝕜 (fun x => (f₂ x).1) x :=
  differentiableAt_fst.comp x h

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