contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt

English

The symmetry (or dual symmetry) of the tangent bundle model-space homeomorphism is C^n.

Русский

Симметрия гомоморфизма касательных пространство-модель гладкая до порядка n.

LaTeX

$$$\text{ContMDiff}_n(\text{tangentBundleModelSpaceHomeomorph},\, \text{symm})$$$

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 contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt {V : Π (x : E), TangentSpace 𝓘(𝕜, E) x} {s : Set E} {x : E} :
    ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent n (fun x ↦ (V x : TangentBundle 𝓘(𝕜, E) E)) s x ↔
      ContDiffWithinAt 𝕜 n V s x :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  ·
    exact
      ContMDiffWithinAt.contDiffWithinAt <|
        (contMDiff_snd_tangentBundle_modelSpace E 𝓘(𝕜, E)).contMDiffAt.comp_contMDiffWithinAt _ h
  · apply Bundle.contMDiffWithinAt_totalSpace.2
    refine ⟨contMDiffWithinAt_id, ?_⟩
    convert h.contMDiffWithinAt with y
    simp

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