English
Final formulation under maximal atlas conditions connecting an in-domain statement to a lifted chart expression.
Русский
Формулировка под условиями максимального атласа связывает утверждение внутри области с выражением через графы перенесенного атласа.
LaTeX
$$theorem contMDiffWithinAt_iff_of_mem_maximalAtlas {x : M} (he : e ∈ maximalAtlas I n M) (he' : e' ∈ maximalAtlas I' n M') (hx : x ∈ e.source) (hy : f x ∈ e'.source) : ContMDiffWithinAt I I' n f s x ↔ ContinuousWithinAt f s x ∧ ContDiffWithinAt 𝕜 n (e'.extend I' ∘ f ∘ (e.extend I).symm) ((e.extend I).symm ⁻¹' s ∩ range I) (e.extend I x)$$
Lean4
/-- One can reformulate being `C^n` within a set at a point as continuity within this set at this
point, and being `C^n` in any chart containing that point. -/
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).symm ⁻¹' s ∩ range I)
(extChartAt I x x') :=
contMDiffWithinAt_iff_of_mem_maximalAtlas (chart_mem_maximalAtlas x) (chart_mem_maximalAtlas y) hx hy
