strict_convex_space): Ray characterization of `∥x - y∥` (#13293)

Commit

3 years ago

feat(analysis/convex/strict_convex_space): Ray characterization of `∥x - y∥` (#13293) `∥x - y∥ = |∥x∥ - ∥y∥|` if and only if `x` and `y` are on the same ray.

Author

YaelDillies

Parents

f1c98ba8

mathlib 483b7df9 - feat(analysis/convex/strict_convex_space): Ray characterization of `∥x - y∥` (#13293)

mathlib
483b7df9 - feat(analysis/convex/strict_convex_space): Ray characterization of `∥x - y∥` (#13293)