Define a predistance on α ⊕ β, for which Φ p and Ψ p are at distance ε

Given two maps Φ and Ψ intro metric spaces α and β such that the distances between Φ p and Φ q, and between Ψ p and Ψ q, coincide up to 2 ε where ε > 0, one can almost glue the two spaces α and β along the images of Φ and Ψ, so that Φ p and Ψ p are at distance ε.

The distance on the disjoint union indeed defines a metric space. All the distance properties follow from our choice of the distance. The harder work is to show that the uniform structure defined by the distance coincides with the disjoint union uniform structure.

The left injection of a space in a disjoint union in an isometry

The right injection of a space in a disjoint union in an isometry

Predistance on the disjoint union Σn, X n.

The predistance on the disjoint union Σn, X n can be computed in any X k for large enough k.

Premetric space structure on Σn, X n.

The type giving the inductive limit in a metric space context.

Metric space structure on the inductive limit.

Mapping each X n to the inductive limit.

The map to_inductive_limit n mapping X n to the inductive limit is an isometry.

The maps to_inductive_limit n are compatible with the maps f n.