hasStrictFDerivAt_equiv_symm — Mathlib

English

The symmetric derivative statement for the inverse of the canonical PiLp equivalence holds.

Русский

Утверждение симметрии для обратного канонического эквивалента PiLp сохраняется.

LaTeX

$$$$ HasStrictFDerivAt\\bigl( (WithLp.equiv p ((i) → E i))^{ -1} \\bigr) \\bigl( (PiLp.continuousLinearEquiv p 𝕜 E)^{ -1} \\bigr). $$$$

Lean4

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

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