hasFDerivAt_equiv_symm — Mathlib

English

The derivative of the inverse equivalence symmetry map is given by the symmetrized continuous linear map of the forward equivalence.

Русский

Производная обратной эквивалентности симметрического отображения задаётся симметрическим непрерывным линейным отображением передней эквивалентности.

LaTeX

$$$ \text{HasFDerivAt}\big( \mathrm{WithLp.equiv} .\mathrm{symm}, (\mathrm{continuousLinearEquiv}(p, 𝕜, \_).\mathrm{symm}).\mathrm{toContinuousLinearMap}, f \big) $$$

Lean4

@[deprecated hasFDerivAt_toLp (since := "2025-05-07")]
theorem hasFDerivAt_equiv_symm (f : ∀ i, E i) :
    HasFDerivAt (WithLp.equiv _ _).symm (continuousLinearEquiv p 𝕜 _).symm.toContinuousLinearMap f :=
  hasFDerivAt_toLp _ f

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