comp_hasFDerivAt_iff' — Mathlib

English

A variant of the HasFDerivAt equivalence with precomposition by iso.

Русский

Вариант эквивалентности HasFDerivAt при предпоследовании через iso.

LaTeX

$$$HasFDerivAt (Function.comp (EquivLike.toFunLike.coe iso) f) (iso.symm.toContinuousLinearMap.comp f') x \iff HasFDerivAt f f' x$$$

Lean4

theorem comp_hasFDerivAt_iff' {f : G → E} {x : G} {f' : G →L[𝕜] F} :
    HasFDerivAt (iso ∘ f) f' x ↔ HasFDerivAt f ((iso.symm : F →L[𝕜] E).comp f') x := by
  simp_rw [← hasFDerivWithinAt_univ, iso.comp_hasFDerivWithinAt_iff']

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