English
A reformulation of differentiability within a set using the target intersection and a lifted chart representation.
Русский
Переоформление дифференцируемости внутри множества через целевое пересечение и представление через lift-Map графа карты.
LaTeX
$$MDifferentiableWithinAt I I' f s x ↔ ContinuousWithinAt f s x ∧ DifferentiableWithinAt 𝕜 (extChartAt I' (f x) ∘ f ∘ (extChartAt I x).symm) ((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)) (extChartAt I x x)$$
Lean4
theorem mdifferentiableWithinAt_iff_target_of_mem_source [IsManifold I' 1 M'] {x : M} {y : M'}
(hy : f x ∈ (chartAt H' y).source) :
MDifferentiableWithinAt I I' f s x ↔
ContinuousWithinAt f s x ∧ MDifferentiableWithinAt I 𝓘(𝕜, E') (extChartAt I' y ∘ f) s x :=
by
simp_rw [MDifferentiableWithinAt]
rw [differentiableWithinAt_localInvariantProp.liftPropWithinAt_indep_chart_target (chart_mem_maximalAtlas y) hy,
and_congr_right]
intro hf
simp_rw [StructureGroupoid.liftPropWithinAt_self_target]
simp_rw [((chartAt H' y).continuousAt hy).comp_continuousWithinAt hf]
rw [← extChartAt_source I'] at hy
simp_rw [(continuousAt_extChartAt' hy).comp_continuousWithinAt hf]
rfl
