contMDiffOn_vectorSpace_iff_contDiffOn

English

The equivalence contMDiffOn_vectorSpace_iff_contDiffOn states that C^n on a set for a vector field is equivalent to C^n on that set in the classical sense.

Русский

Сходимость по порядку n для векторного поля на области эквивалентна классической дифференцируемости на той же области.

LaTeX

$$$ContMDiffOn_{I} \\bigl(tangent\, n, V, s\\bigr) \\iff ContDiffOn_{\\mathcal{I}}(n, V, s)$$$

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 contMDiffOn_vectorSpace_iff_contDiffOn {V : Π (x : E), TangentSpace 𝓘(𝕜, E) x} {s : Set E} :
    ContMDiffOn 𝓘(𝕜, E) 𝓘(𝕜, E).tangent n (fun x ↦ (V x : TangentBundle 𝓘(𝕜, E) E)) s ↔ ContDiffOn 𝕜 n V s := by
  simp only [ContMDiffOn, ContDiffOn, contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt]

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