comp_hasStrictFDerivAt_iff — Mathlib

English

Another formulation of HasFDerivWithinAt under composition with iso: HasFDerivWithinAt (Function.comp (EquivLike.toFunLike.coe iso) f) ((iso : E →L[𝕜] F).comp f') s x.

Русский

Другая запись HasFDerivWithinAt при композиции с iso: HasFDerivWithinAt (Function.comp (toFunLike.coe iso) f) ((iso).comp f') s x.

LaTeX

$$$HasFDerivWithinAt (Function.comp (EquivLike.toFunLike.coe iso) f) ((iso : E →L[𝕜] F).comp f') s x$$$

Lean4

theorem comp_hasStrictFDerivAt_iff {f : G → E} {x : G} {f' : G →L[𝕜] E} :
    HasStrictFDerivAt (iso ∘ f) ((iso : E →L[𝕜] F).comp f') x ↔ HasStrictFDerivAt f f' x :=
  by
  refine ⟨fun H => ?_, fun H => iso.hasStrictFDerivAt.comp x H⟩
  convert iso.symm.hasStrictFDerivAt.comp x H using 1 <;> ext z <;> apply (iso.symm_apply_apply _).symm

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