English
The second projection on a domain is C^∞; that is, for any set s ⊆ E × F, Prod.snd: E × F → F is infinitely differentiable on s.
Русский
Вторая проекция на домене является бесконечно гладкой; для любого множества s ⊆ E × F отображение Prod.snd: E × F → F бесконечно гладко на s.
LaTeX
$$$\forall s:\,\text{Set}(E\times F),\; \operatorname{ContDiff}_{\mathbb{k}}\, n \, (\operatorname{Prod.snd})\, s$.$$
Lean4
/-- The second projection on a domain in a product is `C^∞`. -/
@[fun_prop]
theorem contDiffOn_snd {s : Set (E × F)} : ContDiffOn 𝕜 n (Prod.snd : E × F → F) s :=
ContDiff.contDiffOn contDiff_snd