Mathlib v3 is deprecated. Go to Mathlib v4

Theorem eq_midpoint_of_dist_eq_half

Modification history

2022-06-23 14:10
src/analysis/convex/strict_convex_space.lean
feat(analysis/convex/strict_convex_space): isometries of strictly convex spaces are affine (#14837) …
Added eq_midpoint_of_dist_eq_halfView on Github →