mathlib

a355d88c - feat(topology/metric_space/gluing): metric space structure on sigma types (#11965)

feat(topology/metric_space/gluing): metric space structure on sigma types (#11965) We define a (noncanonical) metric space structure on sigma types (aka arbitrary disjoint unions), as follows. Each piece is isometrically embedded in the union, while for `x` and `y` in different pieces their distance is `dist x x0 + 1 + dist y0 y`, where `x0` and `y0` are basepoints in the respective parts. This is *not* registered as an instance. This definition was already there for sum types (aka disjoint union of two pieces). We also fix this existing definition to avoid `inhabited` assumptions. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>