Commit 2025-07-01 09:03 5c0c2dc5

feat: constructor for emetric space with a preexisting topology (#26503) Consider an extended distance on a topological space for which the balls are neighborhoods of points, and such that any neighborhood contains a ball. Then we define the emetric space structure associated to this distance, with a topology defeq to the initial one.