English
Differentiability within a set at x is equivalent to continuity within the set at x and differentiability in the chart on the target intersection, at the chart point.
Русский
Дифференцируемость внутри множества в точке x эквивалентна непрерывности внутри множества в точке x и дифференцируемости в переходной карте на пересечении целевого множества с доменом, в точке карты.
LaTeX
$$MDifferentiableWithinAt I I' f s x ↔ ContinuousWithinAt f s x ∧ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) ((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s) (extChartAt I x x)$$
Lean4
theorem mdifferentiableWithinAt_iff_target_inter {f : M → M'} {s : Set M} {x : M} :
MDifferentiableWithinAt I I' f s x ↔
ContinuousWithinAt f s x ∧
DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) ((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s)
((extChartAt I x) x) :=
by
rw [mdifferentiableWithinAt_iff']
refine and_congr Iff.rfl (exists_congr fun f' => ?_)
rw [inter_comm]
simp only [HasFDerivWithinAt, nhdsWithin_inter, nhdsWithin_extChartAt_target_eq]
