snd'' — Mathlib

English

The second projection at a point in a product is C^∞; i.e., for p = (x, y), ContDiffAt 𝕜 n (Prod.snd) p holds.

Русский

Вторая проекция в точке произведения является бесконечно гладкой; для p=(x,y) выполняется ContDiffAt 𝕜 n (Prod.snd) p.

LaTeX

$$$\mathrm{ContDiffAt}_{\mathbb{k}} \ n \ (\mathrm{Prod.snd}) p.$$$

Lean4

/-- Precomposing `f` with `Prod.snd` is `C^n` at `x : E × F` -/
theorem snd'' {f : F → G} {x : E × F} (hf : ContDiffAt 𝕜 n f x.2) : ContDiffAt 𝕜 n (fun x : E × F => f x.2) x :=
  hf.comp x contDiffAt_snd

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