Mathlib v3 is deprecated. Go to Mathlib v4

Theorem dist_add_dist_of_mem_segment

Modification history

2023-01-20 23:55
src/analysis/convex/normed.lean
chore(analysis/convex/topology): split (#18187) …
Modified dist_add_dist_of_mem_segmentView on Github →
2022-03-26 20:22
src/analysis/convex/topology.lean
feat(analysis/convex/strict_convex_space): Strictly convex spaces (#11794) …
Added dist_add_dist_of_mem_segmentView on Github →