Commit 2022-04-12 03:21 483b7df9

View on Github →

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.

Estimated changes

Modified src/analysis/complex/arg.lean

modified theorem complex.abs_add_eq

modified theorem complex.abs_add_eq_iff

modified theorem complex.abs_sub_eq

added theorem complex.abs_sub_eq_iff

modified theorem complex.same_ray_iff

modified theorem complex.same_ray_of_arg_eq

Modified src/analysis/convex/strict_convex_space.lean

added theorem abs_lt_norm_sub_of_not_same_ray

added theorem lt_norm_sub_of_not_same_ray

added theorem not_same_ray_iff_abs_lt_norm_sub

added theorem same_ray_iff_norm_sub