Structures · Topology

WeakPseudoEMetricSpace

A WeakPseudoEMetricSpace is a topological space endowed with a ℝ≥0∞-value distance edist which is almost an extended pseudometric space: the edist is reflexive, commutative and satisfies the triangle inequality, but the topology on α need not equal the topology induced by the edist. (It must be at least as fine, and agree with it on eballs of finite radius.) This generalises both pseudo extended metric spaces and ℝ≥0∞ (which have an extended distance, which does not induce the order topology there).

Defined in

Mathlib.Topology.EMetricSpace.Defs

Shape

One type argument · adds edist_self, edist_comm, edist_triangle, topology_le, topology_eq_on_restrict