contDiffOn_snd — Mathlib

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

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