English
A similar equivalence contMDiff_vectorSpace_iff_contDiff states that the manifold C^n agrees with the classical C^n for vector fields on a model space.
Русский
Для векторного пространства совпадают определения в смысле многообразия и классического C^n для векторных полей на моделях пространства.
LaTeX
$$$ContMDiff_{I} n V = ContDiff_{\mathcal{I}} n V$$$
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 contMDiff_vectorSpace_iff_contDiff {V : Π (x : E), TangentSpace 𝓘(𝕜, E) x} :
ContMDiff 𝓘(𝕜, E) 𝓘(𝕜, E).tangent n (fun x ↦ (V x : TangentBundle 𝓘(𝕜, E) E)) ↔ ContDiff 𝕜 n V := by
simp only [← contMDiffOn_univ, ← contDiffOn_univ, contMDiffOn_vectorSpace_iff_contDiffOn]