comp_right_hasFDerivAt_iff' — Mathlib

English

For a function f : F → G and s ⊆ F, the HasFDerivWithinAt for f ∘ iso with derivative f' ∘ iso equals HasFDerivWithinAt of f with derivative f' on s at iso x.

Русский

Для функции f : F → G и подмножества s ⊆ F, HasFDerivWithinAt для f ∘ iso с производной f' ∘ iso эквивалентен HasFDerivWithinAt функции f f' на s в точке iso x.

LaTeX

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

Lean4

theorem comp_right_hasFDerivAt_iff' {f : F → G} {x : E} {f' : E →L[𝕜] G} :
    HasFDerivAt (f ∘ iso) f' x ↔ HasFDerivAt f (f'.comp (iso.symm : F →L[𝕜] E)) (iso x) := by
  simp only [← hasFDerivWithinAt_univ, ← iso.comp_right_hasFDerivWithinAt_iff', preimage_univ]

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