contMDiffWithinAt_iff_of_mem_source'

English

Let x' ∈ M be in the source of the chart at x and f(x') lies in the source of the chart at y. Then f is C^n-differentiable (within the set s at x') if and only if f is continuous within s at x' and, in the chart coordinates, f is C^n-diff on the corresponding domain.

Русский

Пусть x' принадлежит источнику(chartAt H x) и f(x') принадлежит источнику(chartAt H' y). Тогда отображение f является C^n на множестве s в точке x' тогда и только тогда, когда оно непрерывно на s в x' и в координатахchart оно является C^n-дифференцируемым на соответствующей области.

LaTeX

$$$ContMDiffWithinAt I I' n f s x' \;\Longleftrightarrow\; ContinuousWithinAt f s x' \land\quad ContDiffWithinAt 𝕜 n (extChartAt I' y \circ f \circ (extChartAt I x).symm)\;((extChartAt I x).target \cap (extChartAt I x).symm^{-1}(s \cap f^{-1}(extChartAt I' y).source))$$$

Lean4

theorem contMDiffWithinAt_iff_of_mem_source' {x' : M} {y : M'} (hx : x' ∈ (chartAt H x).source)
    (hy : f x' ∈ (chartAt H' y).source) :
    ContMDiffWithinAt I I' n f s x' ↔
      ContinuousWithinAt f s x' ∧
        ContDiffWithinAt 𝕜 n (extChartAt I' y ∘ f ∘ (extChartAt I x).symm)
          ((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
          (extChartAt I x x') :=
  by
  refine (contMDiffWithinAt_iff_of_mem_source hx hy).trans ?_
  rw [← extChartAt_source I] at hx
  rw [← extChartAt_source I'] at hy
  rw [and_congr_right_iff]
  set e := extChartAt I x; set e' := extChartAt I' (f x)
  refine fun hc => contDiffWithinAt_congr_set ?_
  rw [← nhdsWithin_eq_iff_eventuallyEq, ← e.image_source_inter_eq', ← map_extChartAt_nhdsWithin_eq_image' hx, ←
    map_extChartAt_nhdsWithin' hx, inter_comm, nhdsWithin_inter_of_mem]
  exact hc (extChartAt_source_mem_nhds' hy)

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