Theorems · Definition · general topology

Metric.Sigma.metricSpace

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

A metric space structure on the disjoint union Σ i, E i. 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

2 results in Mathlib

Foundations

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

Assumes

MetricSpace