Commit 2026-04-28 22:05 4edf5d90

feat(Topology/EMetricSpace): add Weak(Pseudo)EMetricSpace (#38105) Introduce the concept of Weak(Pseudo)EMetric spaces, some basic properties and proves that the one-point compactification of a Weak(Pseudo)EMetricSpace again has a Weak(Pseudo)EMetricSpace structure. This is inspired by discussion on zulip and based on #27756. In short, types like ENNReal and ENat have a very "metric-like" structure: they are endowed with an ℝ≥0∞-valued edist which is reflexive, commutative and satisfies the triangle inequality --- but their topology is finer than the topology induced by the edist. (Both agree on balls of finite radius.) For this reason, they are not PseudoEMetricSpaces. Introducing this abstraction can make more definitions applicable to ENNReal, such as EVariationOn. A future PR will prove that products and induced (and therefore subtypes) of Weak(Pseudo)EMetricSpaces are such, and add WeakEMetricSpace instances on ENNReal and ENat. (This should be rather easy with the one-point compactification property.)