continuousLinearMap_comp — Mathlib

English

Let f be C^n differentiable on a set s. If g is a continuous linear map from F to G, then the composition g ∘ f is also C^n on s.

Русский

Пусть f имеет гладкость C^n на множестве s. Тогда композиция g ∘ f также имеет гладкость C^n на s, если g: F → G непрерывно линейна.

LaTeX

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

Lean4

/-- Composition by continuous linear maps on the left preserves `C^n` functions on domains. -/
theorem continuousLinearMap_comp (g : F →L[𝕜] G) (hf : ContDiffOn 𝕜 n f s) : ContDiffOn 𝕜 n (g ∘ f) s := fun x hx =>
  (hf x hx).continuousLinearMap_comp g

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