English
A refined variant of the target-intersection formulation for differentiability within a set at a point.
Русский
Уточнённая версия формулировки через целевое пересечение для дифференцируемости внутри множества в точке.
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 mdifferentiableAt_iff_target {x : M} :
MDifferentiableAt I I' f x ↔ ContinuousAt f x ∧ MDifferentiableAt I 𝓘(𝕜, E') (extChartAt I' (f x) ∘ f) x := by
rw [← mdifferentiableWithinAt_univ, ← mdifferentiableWithinAt_univ, mdifferentiableWithinAt_iff_target,
continuousWithinAt_univ]
