contDiff_snd — Mathlib

English

Precomposing with Prod.fst preserves ContDiff: if f is ContDiff, then x ↦ f(x).fst is ContDiff.

Русский

Пре-композиция с Prod.fst сохраняет ContDiff: если f — ContDiff, то x ↦ f(x).fst — ContDiff.

LaTeX

$$$\forall f,\; \ContDiff 𝕜 n f \rightarrow \ContDiff 𝕜 n (\lambda x: f x.1)$$$

Lean4

/-- The second projection in a product is `C^∞`. -/
@[fun_prop]
theorem contDiff_snd : ContDiff 𝕜 n (Prod.snd : E × F → F) :=
  IsBoundedLinearMap.contDiff IsBoundedLinearMap.snd

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