comp_hasFDerivWithinAt_iff' — Mathlib

English

For iso: E ≃L[𝕜] F and any f : G → E, Differentiable 𝕜 (f ∘ iso) x iff Differentiable 𝕜 f x

Русский

Для изоморфизма iso: E ≃L[𝕜] F и любой f : G → E, $f \\circ iso$ дифференцируем в точке x тогда и только тогда, когда f дифференцируем в x.

LaTeX

$$$ \\operatorname{Differentiable}_{\\mathbb{k}}(f \\circ iso) x \\iff \\operatorname{Differentiable}_{\\mathbb{k}} f x $$$

Lean4

theorem comp_hasFDerivWithinAt_iff' {f : G → E} {s : Set G} {x : G} {f' : G →L[𝕜] F} :
    HasFDerivWithinAt (iso ∘ f) f' s x ↔ HasFDerivWithinAt f ((iso.symm : F →L[𝕜] E).comp f') s x :=
  (iso : E ≃L[𝕜] F).comp_hasFDerivWithinAt_iff'

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