[Merged by Bors] - feat(analysis/convex/strict_convex_space): isometries of strictly convex spaces are affine

[jsm28]

Add the result that isometries of (affine spaces for) real normed
spaces with strictly convex codomain are affine isometries. In
particular, this applies to isometries of Euclidean spaces (we already
have the instance that real inner product spaces are uniformly convex
and thus strictly convex). Strict convexity means the surjectivity
requirement of Mazur-Ulam can be avoided.

---

[YaelDillies]

The proofs look golfable, but the rest looks very fine!

[jsm28]

Golfing of proofs is welcome (the intermediate lemmas aren't really intended to be of independent use, and follow immediately from the final results, so if any of those lemmas become redundant after golfing it would be reasonable to remove them).

[urkud]

I would write the main proof using affine_map.of_map_midpoint and the following lemma: if dist x y = r * dist x z and dist y z = (1 - r) * dist x z, then y is the convex combination of x and z with weights (1 - r) and r (proof: since dist x y + dist y z = dist x z, we know that y belongs to the segment; the weights can be found from either eqn).
Possibly, it makes sens to add a version of this lemma with r and r - 1 instead of r and 1 - r too.

[jsm28]

I've reworked the proof using affine_map.of_map_midpoint and the suggested lemma (removing all the other intermediate lemmas and definitions), feel free to golf any of the new proofs.

[urkud]

Reformulated using line_map, golfed.

[urkud]

Please mention this in the module docstring. Otherwise LGTM.
bors d+

[bors]

✌️ jsm28 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[jsm28]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests