hasStrictFDerivAt — Mathlib

English

Let iso be a linear isomorphism E ≃L[𝕜] F. Then HasFDerivWithinAt (f ∘ iso) f' (iso^{-1}' s) x is equivalent to HasFDerivWithinAt f (f' ∘ iso.symm) s (iso x).

Русский

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

@[fun_prop]
protected theorem hasStrictFDerivAt : HasStrictFDerivAt iso (iso : E →L[𝕜] F) x :=
  (iso : E ≃L[𝕜] F).hasStrictFDerivAt

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