snd' — Mathlib

English

If f: F → G is C^n, then the map (x, y) ↦ f(y) is C^n on the product space E × F.

Русский

Пусть f: F → G гладко порядка n; тогда отображение (x, y) ↦ f(y) на произведении E × F гладко порядка n.

LaTeX

$$$\text{If } f: F \to G \text{ is } \mathcal{C}^n, \text{ then } (x,y) \mapsto f(y) \text{ is } \mathcal{C}^n.$$$

Lean4

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

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