continuousLinearMap_comp — Mathlib

English

If g is a linear map and f is ContDiffAt 𝕜 n at x, then g ∘ f is ContDiffAt 𝕜 n at x.

Русский

Если g линейно, и f гладко к точке x, тогда g ∘ f гладко к той же точке.

LaTeX

$$$ (g : F \toL[\mathbb{K}] G) \; \&\; hf : \operatorname{ContDiffWithinAt}_{\mathbb{K}}^{n} f\ s\ x \Rightarrow \operatorname{ContDiffWithinAt}_{\mathbb{K}}^{n} (g \circ f) s x $$$

Lean4

/-- Composition by continuous linear maps on the left preserves `C^n` functions in a domain
at a point. -/
theorem continuousLinearMap_comp (g : F →L[𝕜] G) (hf : ContDiffAt 𝕜 n f x) : ContDiffAt 𝕜 n (g ∘ f) x :=
  ContDiffWithinAt.continuousLinearMap_comp g hf

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