English
If s is a neighborhood of x in the manifold, there is c>0 such that the set of points with riemannian distance less than c is contained in s.
Русский
Если s — окрестность x, существует c>0, такая что {y : riemannian distance < c} ⊆ s.
LaTeX
$$$$\\exists c>0, \\{y: riemannianEDist(I,x,y) < c\\} \\subseteq s.$$$$
Lean4
/-- If points are close for the topology, then their Riemannian distance is small. -/
theorem eventually_riemannianEDist_lt (x : M) {c : ℝ≥0∞} (hc : 0 < c) : ∀ᶠ y in 𝓝 x, riemannianEDist I x y < c :=
by
rcases eventually_riemannianEDist_le_edist_extChartAt I x with ⟨C, C_pos, hC⟩
have : (extChartAt I x) ⁻¹' (EMetric.ball (extChartAt I x x) (c / C)) ∈ 𝓝 x :=
by
apply (continuousAt_extChartAt x).preimage_mem_nhds
exact EMetric.ball_mem_nhds _ (ENNReal.div_pos hc.ne' (by simp))
filter_upwards [this, hC] with y hy h'y
apply h'y.trans_lt
have : edist (extChartAt I x x) (extChartAt I x y) < c / C := by simpa only [mem_preimage, EMetric.mem_ball'] using hy
rwa [ENNReal.lt_div_iff_mul_lt, mul_comm] at this
· exact Or.inl (mod_cast C_pos.ne')
· simp
