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

Merged

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

kim-em merged 4 commits into master from dist-seq

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

722d889b

Add two more versions of the "polygonal" inequality

e51c0926

Use `dist_le_Ico_sum_dist` in `cauchy_seq_of_summable_dist`

cd78e200

Merge branch 'master' into dist-seq

75b59153

kim-em approved these changes on 2019-10-21

kim-em merged 809276c0 into master 6 years ago

urkud deleted the dist-seq branch 6 years ago

Reviewers

kim-em

Assignees

No one assigned

Labels

None yet

Milestone

No milestone