Commit 2023-10-26 14:48 5f703854

View on Github →

feat: Flat triangles have aligned vertices (#7733) In a normed torsor over a strictly convex space, if the triangle inequality dist a c ≤ dist a b + dist b c is an equality, then b lies between a and c.

Estimated changes

Modified Mathlib/Analysis/Convex/Between.lean

added theorem mem_segment_iff_wbtw

Modified Mathlib/Analysis/Convex/Normed.lean

added theorem Wbtw.dist_add_dist

Modified Mathlib/Analysis/Convex/StrictConvexBetween.lean

added theorem Isometry.affineIsometryOfStrictConvexSpace_apply

added theorem Isometry.coe_affineIsometryOfStrictConvexSpace

added theorem dist_add_dist_eq_iff

added theorem eq_lineMap_of_dist_eq_mul_of_dist_eq_mul

added theorem eq_midpoint_of_dist_eq_half

Modified Mathlib/Analysis/Convex/StrictConvexSpace.lean

deleted theorem Isometry.affineIsometryOfStrictConvexSpace_apply

deleted theorem Isometry.coe_affineIsometryOfStrictConvexSpace

deleted theorem dist_add_dist_eq_iff

deleted theorem eq_lineMap_of_dist_eq_mul_of_dist_eq_mul

deleted theorem eq_midpoint_of_dist_eq_half