contMDiffAt_iff_of_mem_source — Mathlib

English

For a point x' in the source of the chart at x and f(x') in the source of the chart at y, being differentiable of order n at x' is equivalent to f being continuous at x' and being C^n in chart coordinates at x and y.

Русский

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

LaTeX

$$$ContMDiffAt I I' n f x' \;\Longleftrightarrow\; (ContinuousAt f x') \,\land\\quad ContDiffWithinAt 𝕜 n (extChartAt I' y \circ f \circ (extChartAt I x).symm)\; (\text{range } I) \;(extChartAt I x x')$$$

Lean4

theorem contMDiffAt_iff_of_mem_source {x' : M} {y : M'} (hx : x' ∈ (chartAt H x).source)
    (hy : f x' ∈ (chartAt H' y).source) :
    ContMDiffAt I I' n f x' ↔
      ContinuousAt f x' ∧
        ContDiffWithinAt 𝕜 n (extChartAt I' y ∘ f ∘ (extChartAt I x).symm) (range I) (extChartAt I x x') :=
  (contMDiffWithinAt_iff_of_mem_source hx hy).trans <| by rw [continuousWithinAt_univ, preimage_univ, univ_inter]

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