Revision #1641 → #1809 · back to history
18e53e76fa4a| Field | From #1641 | To #1809 |
|---|---|---|
| mathlib.decl | riemannianEDist_le_pathELength | Manifold.riemannianEDist_le_pathELength |
| note | riemannianEDist_le_pathELength shows the geodesic (Riemannian) distance lower-bounds any C¹ path length, capturing the curve-minimization idea but not the specific Euclidean straight-line characterization. | Manifold.riemannianEDist_le_pathELength shows the Riemannian distance lower-bounds any C¹ path length, capturing the curve-minimization idea but not the specific Euclidean straight-line characterization. |
c5c144713783