English
Postcomposing a function with Prod.snd is C^n at a point: if f is ContDiffAt 𝕜 n f x, then x ↦ (f x).2 is ContDiffAt 𝕜 n.
Русский
Посткомпозирование f с Prod.snd является C^n в точке: если f — ContDiffAt 𝕜 n f x, то x ↦ (f x)_2 — ContDiffAt 𝕜 n.
LaTeX
$$$\text{If } f: E \to F \times G \text{ and } p=(x, y) \text{ with } f(p)=(f_1(p), f_2(p)), \; \mathrm{ContDiffAt}_{\mathbb{k}} \ n f p \Rightarrow \mathrm{ContDiffAt}_{\mathbb{k}} \ n (\lambda p, f(p)_2) p.$$$
Lean4
/-- Postcomposing `f` with `Prod.snd` is `C^n` at `x` -/
@[fun_prop]
theorem snd {f : E → F × G} {x : E} (hf : ContDiffAt 𝕜 n f x) : ContDiffAt 𝕜 n (fun x => (f x).2) x :=
contDiffAt_snd.comp x hf
