English
If hs is a UniqueDiffWithinAt at p for s and f₂ is differentiable within s at p, then the derivative within s of the first coordinate equals the projection composed with the derivative within s of f₂ at p.
Русский
Если есть UniqueDiffWithinAt для s в p и f₂ дифференцируема внутри s в p, то производная внутри s по первой координате равна проекции, композиции с производной внутри s от f₂ в p.
LaTeX
$$$ fderivWithin 𝕜 (fun x => (f₂ x).1) s x = (fst 𝕜 F G) \circ (fderivWithin 𝕜 f₂ s x) $$$
Lean4
theorem fst (hs : UniqueDiffWithinAt 𝕜 s x) (h : DifferentiableWithinAt 𝕜 f₂ s x) :
fderivWithin 𝕜 (fun x => (f₂ x).1) s x = (fst 𝕜 F G).comp (fderivWithin 𝕜 f₂ s x) :=
h.hasFDerivWithinAt.fst.fderivWithin hs
