contDiff_fst — Mathlib

English

Precomposing with Prod.fst preserves C^n regularity; i.e., if f is C^n, then x ↦ f(x).fst is C^n.

Русский

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

LaTeX

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

Lean4

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

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