Commit 2023-05-20 10:39 0500ff5e

View on Github →

feat: port Analysis.Convex.StrictConvexSpace (#4120)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Convex/StrictConvexSpace.lean

added theorem Isometry.affineIsometryOfStrictConvexSpace_apply

added theorem Isometry.coe_affineIsometryOfStrictConvexSpace

added theorem StrictConvexSpace.ofNormAdd

added theorem StrictConvexSpace.ofNormAddNeTwo

added theorem StrictConvexSpace.ofNormComboLtOne

added theorem StrictConvexSpace.ofNormComboNeOne

added theorem StrictConvexSpace.ofPairwiseSphereNormNeTwo

added theorem StrictConvexSpace.ofStrictConvexClosedUnitBall

added theorem abs_lt_norm_sub_of_not_sameRay

added theorem combo_mem_ball_of_ne

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

added theorem eq_of_norm_eq_of_norm_add_eq

added theorem lt_norm_sub_of_not_sameRay

added theorem norm_add_lt_of_not_sameRay

added theorem norm_combo_lt_of_ne

added theorem norm_midpoint_lt_iff

added theorem not_sameRay_iff_abs_lt_norm_sub

added theorem not_sameRay_iff_norm_add_lt

added theorem openSegment_subset_ball_of_ne

added theorem sameRay_iff_norm_add

added theorem sameRay_iff_norm_sub

added theorem strictConvex_closedBall