Theorems · Inductive type · general topology

WeakPseudoEMetricSpace

(α : Type u) → [τ : TopologicalSpace α] → Type u

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

Cited by

17 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

TopologicalSpace