Revision #2323 → #2995 · back to history
modifiedTriangle inequality (lengths)613a95511f2f
| Field | From #2323 | To #2995 |
|---|
| note | The geometric triangle inequality on side lengths is the metric-space inequality dist x z ≤ dist x y + dist y z, which holds in any (pseudo)metric space including Euclidean point sets. | The geometric triangle inequality on side lengths is the metric-space inequality dist x z ≤ dist x y + dist y z (dist_triangle), which specializes to Euclidean point sets. |
modifiedShortest distance is a straight line4ffcfe27b157
| Field | From #2323 | To #2995 |
|---|
| note | dist_le_range_sum_dist shows the straight-line distance is a lower bound for any polygonal path, but the general curve-minimization statement is only partially captured. | dist_le_range_sum_dist shows straight-line distance lower-bounds any polygonal path, but the general curve-minimization statement is only partially captured. |
modifiedThree inequalities forme459decd91c2
| Field | From #2323 | To #2995 |
|---|
| note | The three side inequalities a+b>c, b+c>a, c+a>b are just three applications of dist_triangle; no dedicated decl encodes this triple form. | The three side inequalities a+b>c, b+c>a, c+a>b are three applications of dist_triangle; no dedicated decl encodes this triple form. |
modifiedSuccinct form of inequality system0d4b622d6b5d
| Field | From #2323 | To #2995 |
|---|
| note | The compact |a−b| < c < a+b form combines the triangle inequality (norm_add_le) and reverse triangle inequality (norm_sub_norm_le), but no single decl states it for triangle sides. | The compact |a−b| < c < a+b form combines norm_add_le and norm_sub_norm_le, but no single decl states it for triangle sides. |
modifiedSharpening by Pythagoras920a2ae1984b
| Field | From #2323 | To #2995 |
|---|
| note | The Pythagorean theorem is formalized as an iff characterizing the right-angle case, of which the article's equality c²=a²+b² is one direction. | The Pythagorean theorem is formalized as an iff characterizing the right-angle case, one direction of which is the article's equality c²=a²+b². |
modifiedPolygon inequalityd70a9ea1aa39
| Field | From #2323 | To #2995 |
|---|
| note | dist_le_range_sum_dist gives dist (f 0) (f n) ≤ ∑ dist (f i) (f (i+1)), the polygon/path inequality for any number of intermediate points in a metric space. | dist_le_range_sum_dist gives dist (f 0) (f n) ≤ ∑ dist (f i) (f (i+1)), the polygon/path inequality in a metric space. |
modifiedShortest curve is a straight line18e53e76fa4a
| Field | From #2323 | To #2995 |
|---|
| note | 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. | Manifold.riemannianEDist_le_pathELength shows the Riemannian distance lower-bounds any C¹ path length, capturing the curve-minimization idea but not the Euclidean straight-line characterization. |
modifiedConverse of triangle inequality8595808230b8
| Field | From #2323 | To #2995 |
|---|
| note | No Mathlib decl establishes existence of a triangle (or its embedding in the plane) from three lengths satisfying the strict inequalities. | No Mathlib decl establishes existence of a triangle from three lengths satisfying the strict inequalities. |
modifiedNorm triangle inequalityb1f3a3f24377
| Field | From #2323 | To #2995 |
|---|
| note | The norm's subadditivity axiom is provided as norm_add_le : ‖a + b‖ ≤ ‖a‖ + ‖b‖. | The norm's subadditivity axiom is norm_add_le : ‖a + b‖ ≤ ‖a‖ + ‖b‖. |
modifiedConvergent sequences are Cauchy72d7cefdb3b9
| Field | From #2323 | To #2995 |
|---|
| note | Filter.Tendsto.cauchySeq shows a sequence tending to a limit is a Cauchy sequence (in any uniform space, generalizing the metric case). | Filter.Tendsto.cauchySeq shows a sequence tending to a limit is a Cauchy sequence, generalizing the metric case to any uniform space. |
modifiedNorm-induced metric8ec21524115c
| Field | From #2323 | To #2995 |
|---|
| note | dist_eq_norm : dist a b = ‖a - b‖ states that the metric on a (semi)normed group is induced by the norm of the difference. | dist_eq_norm : dist a b = ‖a - b‖ states the metric on a (semi)normed group is induced by the norm of the difference. |
modifiedReverse triangle inequality (metric)c5c144713783
| Field | From #2323 | To #2995 |
|---|
| note | The metric-space reverse triangle inequality |dist x z − dist y z| ≤ dist x y is captured by abs_dist_sub_le. | abs_dist_sub_le captures the metric-space reverse triangle inequality |dist x z − dist y z| ≤ dist x y. |
addedSubadditivity of the norm427efb16a373
addedParallelogram law fails for p ≠ 2d1e93ebb44f4
addedCauchy–Schwarz inequality73c85d07864e