comp_differentiableWithinAt_iff — Mathlib

English

Let iso be a linear isomorphism E ≃L[𝕜] F. Then HasFDerivWithinAt (f ∘ iso) f' (iso ⁻¹' s) x is equivalent to HasFDerivWithinAt f (f' ∘ iso.symm) s (iso x).

Русский

Пусть iso — линейный изоморфизм E ≃L[𝕜] F. Тогда HasFDerivWithinAt (f ∘ iso) f' (iso⁻¹' 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.symm) s (iso x)$$$

Lean4

theorem comp_differentiableWithinAt_iff {f : G → E} {s : Set G} {x : G} :
    DifferentiableWithinAt 𝕜 (iso ∘ f) s x ↔ DifferentiableWithinAt 𝕜 f s x :=
  (iso : E ≃L[𝕜] F).comp_differentiableWithinAt_iff

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