comp_right_hasFDerivWithinAt_iff'

English

Let iso be a linear isomorphism E ≃L[𝕜] F and f : F → G. Then HasFDerivWithinAt (f ∘ iso) f' (iso^{-1}' s) x is equivalent to HasFDerivWithinAt f (f' ∘ iso.symm) s (iso x).

Русский

Пусть iso — линейное изоморфизм E ≃L[𝕜] F и f : F → G. Тогда HasFDerivWithinAt (f ∘ iso) f' (iso^{-1} s) x эквивалентно HasFDerivWithinAt f (f' ∘ iso.symm) s (iso x).

LaTeX

$$$ HasFDerivWithinAt (f \\circ iso) f' (iso^{-1} s) x \\iff HasFDerivWithinAt f (f' \\circ iso^{-1}) s (iso x)$$$

Lean4

theorem comp_right_hasFDerivWithinAt_iff' {f : F → G} {s : Set F} {x : E} {f' : E →L[𝕜] G} :
    HasFDerivWithinAt (f ∘ iso) f' (iso ⁻¹' s) x ↔ HasFDerivWithinAt f (f'.comp (iso.symm : F →L[𝕜] E)) s (iso x) := by
  rw [← iso.comp_right_hasFDerivWithinAt_iff, ContinuousLinearMap.comp_assoc, iso.coe_symm_comp_coe,
    ContinuousLinearMap.comp_id]

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