mathlib3

809276c0 - feat(topology/metric_space): polygonal version of the triangle inequality (#1572)

feat(topology/metric_space): polygonal version of the triangle inequality (#1572) * feat(topology/metric_space): "polygon" version of the triangle inequality * Add two more versions of the "polygonal" inequality * Use `dist_le_Ico_sum_dist` in `cauchy_seq_of_summable_dist`