comp_hasFDerivWithinAt_iff' — Mathlib

English

HasFDerivAt (Function.comp (toFun iso) f) ((iso : E →L[𝕜] F).comp f') x iff HasFDerivWithinAt f f' Set.univ x.

Русский

HasFDerivAt (Function.comp (toFun iso) f) ((iso : E →L[𝕜] F).comp f') x эквивалентно HasFDerivWithinAt f f' Set.univ x.

LaTeX

$$$HasFDerivAt (Function.comp (EquivLike.toFunLike.coe iso) f) ((iso : E →L[𝕜] F).comp f') x \iff HasFDerivWithinAt f f' Set.univ 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 := by
  rw [← iso.comp_hasFDerivWithinAt_iff, ← ContinuousLinearMap.comp_assoc, iso.coe_comp_coe_symm,
    ContinuousLinearMap.id_comp]

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