English
If x belongs to the source of a chart e in the maximal atlas, then differentiability within s at x is equivalent to differentiability in the chart's extended form at the image x′ = e x.
Русский
Если x лежит в области определения карты e в максимальном атласе, то дифференцируемость внутри s в точке x эквивалентна дифференцируемости в расширенной карте в точке x' = e x.
LaTeX
$$MDifferentiableWithinAt I I' f s x ↔ MDifferentiableWithinAt 𝓘(𝕜, E) I' (f ∘ (e.extend I).symm) ((e.extend I).symm ⁻¹' s ∩ range I) (e.extend I x)$$
Lean4
theorem mdifferentiableWithinAt_iff_source_of_mem_maximalAtlas [IsManifold I 1 M] (he : e ∈ maximalAtlas I 1 M)
(hx : x ∈ e.source) :
MDifferentiableWithinAt I I' f s x ↔
MDifferentiableWithinAt 𝓘(𝕜, E) I' (f ∘ (e.extend I).symm) ((e.extend I).symm ⁻¹' s ∩ range I) (e.extend I x) :=
by
have h2x := hx; rw [← e.extend_source (I := I)] at h2x
simp_rw [MDifferentiableWithinAt, differentiableWithinAt_localInvariantProp.liftPropWithinAt_indep_chart_source he hx,
StructureGroupoid.liftPropWithinAt_self_source, e.extend_symm_continuousWithinAt_comp_right_iff,
differentiableWithinAtProp_self_source, DifferentiableWithinAtProp, Function.comp, e.left_inv hx,
(e.extend I).left_inv h2x]
rfl
