Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-09 22:07 38796213

View on Github →

feat(combinatorics/additive/salem_spencer): The sphere does not contain arithmetic progressions (#13259) Prove that the frontier of a strictly convex closed set is Salem-Spencer. For this we need

  • simple lemmas about same_ray. This involves renaming same_ray.exists_right_eq_smul/same_ray.exists_left_eq_smul to same_ray.exists_nonneg_left/same_ray.exists_nonneg_right.
  • that the norm in a real normed space is injective on rays.
  • that the midpoint of two points of equal norm has smaller norm, in a strictly convex space

Estimated changes

added theorem norm_midpoint_lt_iff
added theorem norm_inj_on_ray_left
added theorem norm_inj_on_ray_right
modified theorem same_ray_iff_norm_smul_eq