comp_continuousLinearMap — Mathlib

English

The iterated derivative within a set commutes with left composition by a linear isometry, preserving the norm.

Русский

Итерационная производная внутри множества сохраняется под левой композицией линейной изометрии и сохраняет норму.

LaTeX

$$$\|\, iteratedFDerivWithin 𝕜 i (g \circ f) s x \| = \| iteratedFDerivWithin 𝕜 i f s x \|$ for a linear isometry g$$

Lean4

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

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