mathlib3
feat(topology/metric_space): polygonal version of the triangle inequality
#1572

Merged

Commits

feat(topology/metric_space): "polygon" version of the triangle inequality

urkud committed 6 years ago
Add two more versions of the "polygonal" inequality

urkud committed 6 years ago
Use `dist_le_Ico_sum_dist` in `cauchy_seq_of_summable_dist`

urkud committed 6 years ago
Merge branch 'master' into dist-seq

urkud committed 6 years ago