snd — Mathlib

English

If a function f: E → F × G is C^n at a point, then its second projection is C^n at that point.

Русский

Если функция f: E → F × G гладкая порядка n в точке, то её вторая проекция является гладкой порядка n в этой точке.

LaTeX

$$$\text{If } f: E \to F \times G \text{ is ContDiffAt } 𝕜\, n \ f \text{ at } p, \text{ then } (x \mapsto (f(x))_2) \text{ is ContDiffAt } 𝕜\, n \ at p.$$$

Lean4

@[fun_prop]
theorem snd {f : E → F × G} {s : Set E} (hf : ContDiffOn 𝕜 n f s) : ContDiffOn 𝕜 n (fun x => (f x).2) s :=
  contDiff_snd.comp_contDiffOn hf

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