snd' — Mathlib

English

The second projection map on a product is C^∞ on a domain: ContDiffOn 𝕜 n (Prod.snd) s for any s.

Русский

Вторая проекция на произведении является бесконечно гладкой на домене: ContDiffOn 𝕜 n (Prod.snd) s.

LaTeX

$$$\forall s,\ ContDiffOn_{\mathbb{k}}\, n\ (\mathrm{Prod.snd})\ s.$$

Lean4

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

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