comp_fderivWithin — Mathlib

English

Let iso be a linear isometry E ≃ F. For any f : G → E and any s ⊆ G and x ∈ s, the Fréchet derivative within s satisfies fderivWithin 𝕜 (iso ∘ f) s x = (iso : E →L[𝕜] F) ∘ (fderivWithin 𝕜 f s x).

Русский

Пусть iso — линейная изометрия E ≃ F. Для любой f: G → E, множества s ⊆ G и точки x ∈ s выполняется равенство внутри области: fderivWithin 𝕜 (iso ∘ f) s x = (iso : E →L[𝕜] F) ∘ (fderivWithin 𝕜 f s x).

LaTeX

$$$$ fderivWithin 𝕜 (\\mathrm{iso} \\circ f)\\ s\\ x = (\\mathrm{iso} : E \\to L[𝕜] F) .\\comp\\ (fderivWithin 𝕜 f\\ s\\ x) $$$$

Lean4

theorem comp_fderivWithin {f : G → E} {s : Set G} {x : G} (hxs : UniqueDiffWithinAt 𝕜 s x) :
    fderivWithin 𝕜 (iso ∘ f) s x = (iso : E →L[𝕜] F).comp (fderivWithin 𝕜 f s x) :=
  (iso : E ≃L[𝕜] F).comp_fderivWithin hxs

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