Theorems · Theorem · global analysis

hasFDerivWithinAt_euclidean

∀ {𝕜 : Type u_1} {ι : Type u_2} {H : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup H]
  [inst_2 : NormedSpace 𝕜 H] {f : H → EuclideanSpace 𝕜 ι} {f' : H →L[𝕜] EuclideanSpace 𝕜 ι} {t : Set H} {y : H}
  [Finite ι],
  HasFDerivWithinAt f f' t y ↔
    ∀ (i : ι), HasFDerivWithinAt (fun x => (f x).ofLp i) (PiLp.proj 2 (fun x => 𝕜) i ∘SL f') t y

Defined in

Mathlib.Analysis.InnerProductSpace.Calculus

Cited by

0 results in Mathlib

Foundations

Depth 227 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeNormedAddCommGroupNormedSpaceFinite