feat(topology/metric_space/emetric_space): polygonal inequalities (#1736)
feat(topology/metric_space/emetric_space): polygonal inequalities (#1736)

Migrate #1572 from `dist` to `edist`
leanprover-community/mathlib,leanprover-community/mathlib