contDiffAt_snd — Mathlib

English

If a function f: E → F × G is ContDiffOn 𝕜 n on a set s, then the second projection x ↦ (f x)_2 is ContDiffOn 𝕜 n on s.

Русский

Если функция f: E → F × G является ContDiffOn 𝕜 n на множествах s, то вторая проекция x ↦ (f x)_2 является ContDiffOn 𝕜 n на s.

LaTeX

$$$\mathrm{ContDiffOn}_{\mathbb{k}} \ n \ f\ s \implies \mathrm{ContDiffOn}_{\mathbb{k}} \ n \ (\lambda x, (f x)_2)\ s . $$$

Lean4

/-- The second projection at a point in a product is `C^∞`. -/
@[fun_prop]
theorem contDiffAt_snd {p : E × F} : ContDiffAt 𝕜 n (Prod.snd : E × F → F) p :=
  contDiff_snd.contDiffAt

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