contMDiffAt_iff_source_of_mem_source

English

If a point x′ lies in the source of the local chart at x, then being C^n within a subset s at x′ is equivalent to a lifted chart formulation with the local source considered.

Русский

Если точка x′ лежит в источнике локального графа при x, то быть $C^n$ внутри множества s в x′ эквивалентно переносной формулировке через графы.

LaTeX

$$contMDiffWithinAt_iff_of_mem_source I I' n f s x' hx' hy$$

Lean4

theorem contMDiffAt_iff_source_of_mem_source [IsManifold I n M] {x' : M} (hx' : x' ∈ (chartAt H x).source) :
    ContMDiffAt I I' n f x' ↔
      ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ (extChartAt I x).symm) (range I) (extChartAt I x x') :=
  by simp_rw [ContMDiffAt, contMDiffWithinAt_iff_source_of_mem_source hx', preimage_univ, univ_inter]

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