English
A composition formula for mfderiv holds with the Euclidean model and the chart.
Русский
Сочетание mfderiv с моделью Евклида и чартом удовлетворяет формуле композиции.
LaTeX
$$$((\mathrm{ContinuousLinearMap}.fst) \circ (\mathrm{proj}\ i)) \circ (mfderiv I \; \mathcal I(f.embeddingPiTangent)) = mfderiv I I (chartAt H (f.c (f.ind x hx)))$$$
Lean4
/-- Baby version of the **Whitney weak embedding theorem**: if `M` admits a finite covering by
supports of bump functions, then for some `n` it can be immersed into the `n`-dimensional
Euclidean space. -/
theorem exists_immersion_euclidean {ι : Type*} [Finite ι] (f : SmoothBumpCovering ι I M) :
∃ (n : ℕ) (e : M → EuclideanSpace ℝ (Fin n)),
ContMDiff I (𝓡 n) ∞ e ∧ Injective e ∧ ∀ x : M, Injective (mfderiv I (𝓡 n) e x) :=
by
cases nonempty_fintype ι
set F := EuclideanSpace ℝ (Fin <| finrank ℝ (ι → E × ℝ))
letI : IsNoetherian ℝ (E × ℝ) := IsNoetherian.iff_fg.2 inferInstance
letI : FiniteDimensional ℝ (ι → E × ℝ) := IsNoetherian.iff_fg.1 inferInstance
set eEF : (ι → E × ℝ) ≃L[ℝ] F := ContinuousLinearEquiv.ofFinrankEq finrank_euclideanSpace_fin.symm
refine
⟨_, eEF ∘ f.embeddingPiTangent, eEF.toDiffeomorph.contMDiff.comp f.embeddingPiTangent.contMDiff,
eEF.injective.comp f.embeddingPiTangent_injective, fun x => ?_⟩
rw [mfderiv_comp _ eEF.differentiableAt.mdifferentiableAt
(f.embeddingPiTangent.contMDiff.mdifferentiableAt (mod_cast le_top)),
eEF.mfderiv_eq]
exact eEF.injective.comp (f.embeddingPiTangent_injective_mfderiv _ trivial)
