Mathlib Changelog
v4
Changelog
About
Github
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