English
An alternate formulation of the atlas-based equivalence for differentiability within a set.
Русский
Альтернатива атласной эквивалентности для дифференцируемости внутри множества.
LaTeX
$$MDifferentiableWithinAt I I' f s x ↔ ContinuousWithinAt f s x ∧ DifferentiableOn 𝕜 (extChartAt I' y ∘ f ∘ (extChartAt I x).symm) (Set.image (extChartAt I x).toFun s) ((extChartAt I x).toFun x)$$
Lean4
/-- Differentiability on a set is equivalent to differentiability in the extended charts. -/
theorem mdifferentiableOn_iff_of_mem_maximalAtlas' (he : e ∈ maximalAtlas I 1 M) (he' : e' ∈ maximalAtlas I' 1 M')
(hs : s ⊆ e.source) (h2s : MapsTo f s e'.source) :
MDifferentiableOn I I' f s ↔ DifferentiableOn 𝕜 (e'.extend I' ∘ f ∘ (e.extend I).symm) (e.extend I '' s) :=
(mdifferentiableOn_iff_of_mem_maximalAtlas he he' hs h2s).trans <|
and_iff_right_of_imp fun h ↦ (e.continuousOn_writtenInExtend_iff hs h2s).1 h.continuousOn
