Theorems · Definition · general topology

Metric.Sigma.dist

{ι : Type u_1} → {E : ι → Type u_2} → [(i : ι) → MetricSpace (E i)] → (i : ι) × E i → (i : ι) × E i → ℝ

Distance on a disjoint union. There are many (noncanonical) ways to put a distance compatible with each factor. We choose a construction that works for unbounded spaces, but requires basepoints, chosen arbitrarily. We embed isometrically each factor, set the basepoints at distance 1, arbitrarily, and say that the distance from a to b is the sum of the distances of a and b to their respective basepoints, plus the distance 1 between the basepoints. Since there is an arbitrary choice in this construction, it is not an instance by default.

Defined in

Mathlib.Topology.MetricSpace.Gluing

Cited by

0 results in Mathlib

Foundations

Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MetricSpace