Theorems · Theorem · global analysis

contDiff_euclidean

∀ {𝕜 : Type u_1} {ι : Type u_2} {H : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup H]
  [inst_2 : NormedSpace 𝕜 H] {f : H → EuclideanSpace 𝕜 ι} [inst_3 : Fintype ι] {n : WithTop ℕ∞},
  ContDiff 𝕜 n f ↔ ∀ (i : ι), ContDiff 𝕜 n fun x => (f x).ofLp i

Defined in

Mathlib.Analysis.InnerProductSpace.Calculus

Cited by

1 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupNormedSpaceFintype