English
A Continuous Linear Equivalence has MF-derivative at x equal to its derivative map.
Русский
У непрерывно линейного эквивалентного отображения имеется MF-производная в точке x, равная его производной.
LaTeX
$$HasMFDerivAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') (EquivLike.toFunLike.coe f) x (f.toContinuousLinearMap)$$
Lean4
theorem hasMFDerivAt_id (x : M) : HasMFDerivAt I I (@id M) x (ContinuousLinearMap.id 𝕜 (TangentSpace I x)) :=
by
refine ⟨continuousAt_id, ?_⟩
have : ∀ᶠ y in 𝓝[range I] (extChartAt I x) x, (extChartAt I x ∘ (extChartAt I x).symm) y = y :=
by
apply Filter.mem_of_superset (extChartAt_target_mem_nhdsWithin x)
mfld_set_tac
apply HasFDerivWithinAt.congr_of_eventuallyEq (hasFDerivWithinAt_id _ _) this
simp only [mfld_simps]
