continuousLinearMap_comp — Mathlib

English

If f is C^n (globally) and g is a continuous linear map, then the composition g ∘ f is C^n (globally).

Русский

Если f гладко дифференцируема степенью n на всей области, то композиция с линейным отображением слева сохраняет ту же степень гладкости.

LaTeX

$$$\forall g\colon F \to_L[\mathbb{K}] G,\; \text{ContDiff}_{\mathbb{K}}^{n}(f) \Rightarrow \text{ContDiff}_{\mathbb{K}}^{n}(g\circ f).$$$

Lean4

/-- Composition by continuous linear maps on the left preserves `C^n` functions. -/
theorem continuousLinearMap_comp {f : E → F} (g : F →L[𝕜] G) (hf : ContDiff 𝕜 n f) : ContDiff 𝕜 n fun x => g (f x) :=
  contDiffOn_univ.1 <| ContDiffOn.continuousLinearMap_comp _ (contDiffOn_univ.2 hf)

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