Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-12 22:46 c749cc93

View on Github →

chore(analysis/convex/strict_convex_space): generalize/add strict_convex_space.of_* lemmas (#17206)

Estimated changes

Modified src/analysis/convex/segment.lean

added theorem open_segment_subset_union

Modified src/analysis/convex/strict_convex_space.lean

modified theorem strict_convex_space.of_norm_add

deleted theorem strict_convex_space.of_norm_add_lt

deleted theorem strict_convex_space.of_norm_add_lt_aux

added theorem strict_convex_space.of_norm_add_ne_two

added theorem strict_convex_space.of_norm_combo_lt_one

added theorem strict_convex_space.of_norm_combo_ne_one

added theorem strict_convex_space.of_pairwise_sphere_norm_ne_two

Modified src/analysis/convex/topology.lean

Modified src/analysis/convex/uniform.lean