English
If s is a neighborhood of x, there is a positive c such that the sublevel set of riemannian distance less than c around x is contained in s.
Русский
Если s является окрестностью x, существует позитивная константа c, такая что множество точек с riemannian расстоянием меньше c от x содержится в s.
LaTeX
$$$$\\exists c>0, \\; \\{y:\\ riemannianEDist(I,x,y) < c\\} \\subseteq s.$$$$
Lean4
theorem eventually_norm_mfderivWithin_symm_extChartAt_lt (x : M) :
∃ C > 0, ∀ᶠ y in 𝓝[range I] (extChartAt I x x), ‖mfderivWithin 𝓘(ℝ, E) I (extChartAt I x).symm (range I) y‖ < C :=
by
rcases eventually_norm_mfderivWithin_symm_extChartAt_comp_lt I x with ⟨C, C_pos, hC⟩
refine ⟨C, C_pos, ?_⟩
have : 𝓝 x = 𝓝 ((extChartAt I x).symm (extChartAt I x x)) := by simp
rw [this] at hC
have : ContinuousAt (extChartAt I x).symm (extChartAt I x x) := continuousAt_extChartAt_symm _
filter_upwards [nhdsWithin_le_nhds (this.preimage_mem_nhds hC), extChartAt_target_mem_nhdsWithin x] with y hy h'y
have : y = (extChartAt I x) ((extChartAt I x).symm y) := by simp [-extChartAt, h'y]
simp only [preimage_setOf_eq, mem_setOf_eq] at hy
convert hy
