fst — Mathlib

English

If a function f₂: E → F × G is differentiable at a point x, then the derivative of its first component at x is the projection onto F composed with the derivative of f₂ at x; i.e., D[(f₂)_1](x) = π_1 ∘ Df₂(x).

Русский

Если функция f₂: E → F × G дифференцируема в точке x, то производная её первой компоненты в x равна проекции π_1 ∘ Df₂(x); т.е. D[(f₂)_1](x) = π_1 ∘ Df₂(x).

LaTeX

$$$ fderiv 𝕜 (fun x => (f₂ x).1) x = (fst 𝕜 F G) \circ (fderiv 𝕜 f₂ x) $$$

Lean4

theorem fst (h : DifferentiableAt 𝕜 f₂ x) : fderiv 𝕜 (fun x => (f₂ x).1) x = (fst 𝕜 F G).comp (fderiv 𝕜 f₂ x) :=
  h.hasFDerivAt.fst.fderiv

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