Theorems · Theorem · global analysis

contDiffWithinAt_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} [inst_3 : Fintype ι] {n : WithTop ℕ∞},
  ContDiffWithinAt 𝕜 n f t y ↔ ∀ (i : ι), ContDiffWithinAt 𝕜 n (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

RCLikeNormedAddCommGroupNormedSpaceFintype