comp_right_differentiableWithinAt_iff

English

HasFDerivAt (iso ∘ f) ((iso) ∘ f') x iff HasFDerivAt f f' x.

Русский

HasFDerivAt (iso ∘ f) ((iso) ∘ f') x эквивалентно HasFDerivAt f f' x.

LaTeX

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

Lean4

theorem comp_right_differentiableWithinAt_iff {f : F → G} {s : Set F} {x : E} :
    DifferentiableWithinAt 𝕜 (f ∘ iso) (iso ⁻¹' s) x ↔ DifferentiableWithinAt 𝕜 f s (iso x) :=
  by
  refine ⟨fun H => ?_, fun H => H.comp x iso.differentiableWithinAt (mapsTo_preimage _ s)⟩
  have : DifferentiableWithinAt 𝕜 ((f ∘ iso) ∘ iso.symm) s (iso x) :=
    by
    rw [← iso.symm_apply_apply x] at H
    apply H.comp (iso x) iso.symm.differentiableWithinAt
    intro y hy
    simpa only [mem_preimage, apply_symm_apply] using hy
  rwa [Function.comp_assoc, iso.self_comp_symm] at this

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