comp_differentiable_iff — Mathlib

English

For iso: E ≃L[𝕜] F, {f : F → G} {s : Set F} {x : E} {f' : F →L[𝕜] G}, HasFDerivWithinAt (f ∘ iso) (f' ∘ iso) (iso^{-1} s) x ↔ HasFDerivWithinAt f f' s (iso x).

Русский

Для изоморфизма iso: E ≃L[𝕜] F верна эквивалентность HasFDerivWithinAt (f ∘ iso) (f' ∘ iso) (iso^{-1} s) x ⇔ 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_differentiable_iff {f : G → E} : Differentiable 𝕜 (iso ∘ f) ↔ Differentiable 𝕜 f :=
  (iso : E ≃L[𝕜] F).comp_differentiable_iff

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