mdifferentiableAt_iff_of_mem_source

English

A variant of the atlas-based reformulation using the prime extended chart maps.

Русский

Вариант атласной формы через производные карты с prime расширения.

LaTeX

$$MDifferentiableWithinAt I I' f s x ↔ ContinuousWithinAt f s x ∧ DifferentiableOn 𝕜 (e'.extend I' ∘ f ∘ (e.extend I).symm) (e.extend I '' s)$$

Lean4

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

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