hasStrictFDerivAt_equiv — Mathlib

English

There is a strict derivative for the coordinatewise evaluation map onto the PiLp representation, via the equivalence.

Русский

Существует строгая производная отображения по координатам, переводимого в представление PiLp, через эквив.

LaTeX

$$$$ HasStrictFDerivAt\\bigl( WithLp.toLp p \\bigr) \\bigl( (PiLp.continuousLinearEquiv p 𝕜 E).toContinuousLinearMap f \\bigr). $$$$

Lean4

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

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