English
The Riemannian distance satisfies the triangle inequality: d(x,z) ≤ d(x,y) + d(y,z).
Русский
Неравенство треугольника для расстояния Римана: d(x,z) ≤ d(x,y) + d(y,z).
LaTeX
$$riemannianEDist I x z ≤ riemannianEDist I x y + riemannianEDist I y z$$
Lean4
/-- If some `r` is strictly larger than the Riemannian edistance between two points, there exists
a path between these two points of length `< r`. Here, we get such a path on `[0, 1]`.
For a more precise version giving locally constant paths around the endpoints, see
`exists_lt_locally_constant_of_riemannianEDist_lt` -/
theorem exists_lt_of_riemannianEDist_lt (hr : riemannianEDist I x y < r) :
∃ γ : ℝ → M, γ 0 = x ∧ γ 1 = y ∧ ContMDiffOn 𝓘(ℝ) I 1 γ (Icc 0 1) ∧ pathELength I γ 0 1 < r :=
by
simp only [riemannianEDist, iInf_lt_iff, exists_prop] at hr
rcases hr with ⟨γ, γ_smooth, hγ⟩
refine ⟨γ ∘ (projIcc 0 1 zero_le_one), by simp, by simp, contMDiffOn_comp_projIcc_iff.2 γ_smooth, ?_⟩
rwa [← lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc]
