English
A reformulation of differentiability within a set at a point in terms of continuity on the set and a chartwise differentiability in the target chart after a lift.
Русский
Переформулировка дифференцируемости внутри множества в точке через непрерывность на множестве и дифференцируемость в целевой карте после лифта.
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
/-- One can reformulate smoothness within a set at a point as continuity within this set at this
point, and smoothness in the corresponding extended chart in the target. -/
theorem mdifferentiableWithinAt_iff_target :
MDifferentiableWithinAt I I' f s x ↔
ContinuousWithinAt f s x ∧ MDifferentiableWithinAt I 𝓘(𝕜, E') (extChartAt I' (f x) ∘ f) s x :=
by
simp_rw [MDifferentiableWithinAt, liftPropWithinAt_iff', ← and_assoc]
have cont : ContinuousWithinAt f s x ∧ ContinuousWithinAt (extChartAt I' (f x) ∘ f) s x ↔ ContinuousWithinAt f s x :=
and_iff_left_of_imp <| (continuousAt_extChartAt _).comp_continuousWithinAt
simp_rw [cont, DifferentiableWithinAtProp, extChartAt, OpenPartialHomeomorph.extend, PartialEquiv.coe_trans,
ModelWithCorners.toPartialEquiv_coe, OpenPartialHomeomorph.coe_coe, modelWithCornersSelf_coe, chartAt_self_eq,
OpenPartialHomeomorph.refl_apply]
rfl
