hasFDerivWithinAt_piLp — Mathlib

English

The within-derivative of a PiLp-valued map is equivalent to the family of within-derivatives of its coordinate maps.

Русский

В рамках внутри-на отображении в PiLp производная эквивалентна множеству внутри-производных координатных отображений.

LaTeX

$$$$ HasFDerivWithinAt f\\, f'\\, t\\, y \\iff \\forall i, HasFDerivWithinAt (fun x => f x i) ((PiLp.proj p E i) \\circ f') \\; t \\; y. $$$$

Lean4

theorem hasFDerivWithinAt_piLp :
    HasFDerivWithinAt f f' t y ↔ ∀ i, HasFDerivWithinAt (fun x => f x i) (PiLp.proj _ _ i ∘L f') t y :=
  by
  rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_hasFDerivWithinAt_iff, hasFDerivWithinAt_pi']
  rfl

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