English
For x in M', the symmetric derivative MDifferentiableAt I' I e.symm x holds, mirroring the previous at point statement.
Русский
Для x в M' верно существование производной отражения в точке x, аналогично предыдущему утверждению.
LaTeX
$$$\mathrm{MDifferentiableAt}(I',I, e^{\mathrm{symm}}, x)$$$
Lean4
theorem symm_comp_deriv {x : M} (hx : x ∈ e.source) :
(mfderiv I' I e.symm (e x)).comp (mfderiv I I' e x) = ContinuousLinearMap.id 𝕜 (TangentSpace I x) :=
by
have : mfderiv I I (e.symm ∘ e) x = (mfderiv I' I e.symm (e x)).comp (mfderiv I I' e x) :=
mfderiv_comp x (he.mdifferentiableAt_symm (e.map_source hx)) (he.mdifferentiableAt hx)
rw [← this]
have : mfderiv I I (_root_.id : M → M) x = ContinuousLinearMap.id _ _ := mfderiv_id
rw [← this]
apply Filter.EventuallyEq.mfderiv_eq
have : e.source ∈ 𝓝 x := e.open_source.mem_nhds hx
exact Filter.mem_of_superset this (by mfld_set_tac)
