contMDiff_vectorSpace_iff_contDiff

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]

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