contMDiffAt_vectorSpace_iff_contDiffAt

English

A vector field on a vector space is C^n in the manifold sense iff it is C^n in the vector-space sense.

Русский

Векторное поле на векторном пространстве гладко до порядка n в смысле многообразия тогда и только тогда, когда гладко в смысле векторного пространства.

LaTeX

$$ContMDiffWithinAt ↔ ContDiffWithinAt; ContMDiffOn ↔ ContDiffOn; ContMDiff ↔ ContDiff$$

Lean4

/-- A vector field on a vector space is `C^n` in the manifold sense iff it is `C^n` in the vector
space sense. -/
theorem contMDiffAt_vectorSpace_iff_contDiffAt {V : Π (x : E), TangentSpace 𝓘(𝕜, E) x} {x : E} :
    ContMDiffAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent n (fun x ↦ (V x : TangentBundle 𝓘(𝕜, E) E)) x ↔ ContDiffAt 𝕜 n V x := by
  simp only [← contMDiffWithinAt_univ, ← contDiffWithinAt_univ, contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt]

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