Theorems · Theorem · global analysis

differentiableWithinAt_euclidean

∀ {𝕜 : Type u_1} {ι : Type u_2} {H : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup H]
  [inst_2 : NormedSpace 𝕜 H] {f : H → EuclideanSpace 𝕜 ι} {t : Set H} {y : H} [Finite ι],
  DifferentiableWithinAt 𝕜 f t y ↔ ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x => (f x).ofLp i) 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