English
There exists, near x, a bound C>0 such that the norm of mfderivWithin of the symm extChartAt is uniformly bounded by C.
Русский
Существуют окрестности точки x, где норма mfderivWithin симметричной extChartAt ограничена сверху константой C.
LaTeX
$$$$\\exists C>0\\;\\forall^\\! y\\in ((extChartAt I x).toFun y) ,\\; \\|mfderivWithin(I, I, (extChartAt I x).symm, (range I.toFun'))(y)\\| < C.$$$$
Lean4
theorem eventually_norm_mfderivWithin_symm_extChartAt_comp_lt (x : M) :
∃ C > 0, ∀ᶠ y in 𝓝 x, ‖mfderivWithin 𝓘(ℝ, E) I (extChartAt I x).symm (range I) (extChartAt I x y)‖ < C :=
by
rcases eventually_norm_symmL_trivializationAt_lt E (fun (x : M) ↦ TangentSpace I x) x with ⟨C, C_pos, hC⟩
refine ⟨C, C_pos, ?_⟩
have hx : (chartAt H x).source ∈ 𝓝 x := chart_source_mem_nhds H x
filter_upwards [hC, hx] with y hy h'y
rw [TangentBundle.symmL_trivializationAt h'y] at hy
have A : (extChartAt I x).symm (extChartAt I x y) = y := (extChartAt I x).left_inv (by simpa using h'y)
convert hy using 3 <;> congr
