comp_right_hasFDerivAt_iff — Mathlib

English

For a function f: F → G and iso: E ≃L[𝕜] F, the HasFDerivAt of f ∘ iso equals HasFDerivAt of f after composing with iso, i.e., HasFDerivAt (f ∘ iso) (f' ∘ iso) x ↔ HasFDerivAt f f' (iso x).

Русский

Для функции f : F → G и iso: E ≃L[𝕜] F верна эквивалентность HasFDerivAt: HasFDerivAt (f ∘ iso) (f' ∘ iso) x ↔ HasFDerivAt f f' (iso x).

LaTeX

$$$ HasFDerivAt (f \\circ iso) (f' \\circ iso) x \\iff HasFDerivAt f f' (iso x)$$$

Lean4

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

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