isometry

An isometry (also known as isometric embedding) is a map preserving the edistance between emetric spaces, or equivalently the distance between metric space.

isometry_emetric_iff_metric

On metric spaces, a map is an isometry if and only if it preserves distances.

isometry.edist_eq

An isometry preserves edistances.

isometry.dist_eq

An isometry preserves distances.

isometry.injective

An isometry is injective

isometry_subsingleton

Any map on a subsingleton is an isometry

isometry_id

The identity is an isometry

isometry.comp

The composition of isometries is an isometry

isometry.uniform_embedding

An isometry is an embedding

isometry.continuous

An isometry is continuous.

isometry.inv

The inverse of an isometry is an isometry.

emetric.isometry.diam_image

Isometries preserve the diameter

isometry_subtype_val

The injection from a subtype is an isometry

metric.isometry.diam_image

An isometry preserves the diameter in metric spaces

isometric

α and β are isometric if there is an isometric bijection between them.

isometry.isometric_on_range

An isometry induces an isometric isomorphism between the source space and the range of the isometry.

Kuratowski_embedding.embedding_of_subset

A metric space can be embedded in l^∞(ℝ) via the distances to points in a fixed countable set, if this set is dense. This map is given in the next definition, without density assumptions.

Kuratowski_embedding.embedding_of_subset_dist_le

The embedding map is always a semi-contraction.

Kuratowski_embedding.embedding_of_subset_isometry

When the reference set is dense, the embedding map is an isometry on its image.

Kuratowski_embedding.exists_isometric_embedding

Every separable metric space embeds isometrically in ℓ_infty_ℝ.

Kuratowski_embedding

The Kuratowski embedding is an isometric embedding of a separable metric space in ℓ^∞(ℝ)

Kuratowski_embedding.isometry

The Kuratowski embedding is an isometry

nonempty_compacts.Kuratowski_embedding

Version of the Kuratowski embedding for nonempty compacts